0 | module Deriving.SpecialiseData

   2 | import Control.Monad.Either

   3 | import Control.Monad.Trans

   4 | import public Data.DPair

   5 | import Data.Either

   6 | import Data.Fin.Set

   7 | import Data.List

   8 | import public Data.List.Map -- workaround for compiler bug #2439

   9 | import Data.List.Quantifiers

  10 | import Data.List1

  11 | import Data.Maybe

  12 | import Data.SnocList

  13 | import Data.SnocList.Quantifiers

  14 | import Data.SortedMap

  15 | import Data.SortedMap.Dependent

  16 | import Data.SortedSet

  17 | import Data.Vect

  18 | import Data.Vect.Quantifiers

  19 | import public Decidable.Decidable

  20 | import public Decidable.Equality

  21 | import Deriving.Show

  22 | import public Language.Mk

  23 | import Language.Reflection.Compat

  24 | import Language.Reflection.Compat.Constr

  25 | import public Language.Reflection.Compat.TypeInfo -- workaround for compiler bug #2439

  26 | import Language.Reflection.Expr

  27 | import Language.Reflection.Syntax

  28 | import Language.Reflection.Logging

  29 | import public Language.Reflection.Unify.Interface

  30 | import public Language.Reflection.VarSubst -- workaround for compiler bug #2439

  31 | import Syntax.IHateParens

  33 | %language ElabReflection

  35 | %default total

  43 | data SpecialisationError : Type where

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

  45 |   TaskTypeExtractionError   : SpecialisationError

  46 |   ||| Unused variable

  47 |   UnusedVarError            : SpecialisationError

  48 |   ||| Partial specification

  49 |   PartialSpecError          : SpecialisationError

  50 |   ||| Internal error

  51 |   InternalError             : String -> SpecialisationError

  52 |   ||| Lambda has unnamed arguments

  53 |   UnnamedArgInLambdaError   : SpecialisationError

  54 |   ||| Polymorphic type has unnamed arguments

  55 |   UnnamedArgInPolyTyError   : Name -> SpecialisationError

  56 |   ||| Failed to get TypeInfo

  60 |   MissingTypeInfoError      : Name -> SpecialisationError

  64 | showSE : Show SpecialisationError

  65 | showSE = %runElab derive

  72 | record SpecTask where

  73 |   constructor MkSpecTask

  74 |   ||| Full unification task

  75 |   tqArgs              : List Arg

  76 |   tqRet               : TTImp

  77 |   {auto 0 tqArgsNamed : All IsNamedArg tqArgs}

  78 |   ||| Unification task type

  79 |   ttArgs              : List Arg

  80 |   {auto 0 ttArgsNamed : All IsNamedArg ttArgs}

  81 |   ||| Namespace in which specialiseData was called

  82 |   currentNs           : Namespace

  83 |   ||| Name of specialised type

  84 |   resultName          : Name

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

  86 |   fullInvocation      : TTImp

  87 |   ||| Invocation of specialised type given default arguents

  88 |   specInvocation      : TTImp

  89 |   ||| Polymorphic type's TypeInfo

  90 |   polyTy              : TypeInfo

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

  92 |   {auto 0 polyTyNamed : AllTyArgsNamed polyTy}

  94 | Show SpecTask where

  95 |   showPrec p t =

  96 |     showCon p "SpecTask" $ joinBy "" $

  97 |       [ showArg t.tqArgs

  98 |       , showArg t.tqRet

  99 |       , showArg t.ttArgs

 100 |       , showArg t.currentNs

 101 |       , showArg t.resultName

 102 |       , showArg t.fullInvocation

 103 |       , showArg t.specInvocation

 104 |       , showArg "<polyTy>"

 105 |       ]

 108 | UniResults : Type

 109 | UniResults = List UnificationVerdict

 115 | public export

 116 | record SpecialisationParams where

 117 |   [noHints]

 118 |   constructor MkSpecParams

 119 |   eraseConNames : Bool

 121 | public export

 123 | SpecialisationDefaults : SpecialisationParams

 124 | SpecialisationDefaults = MkSpecParams

 125 |   { eraseConNames = False

 126 |   }

 128 | public export

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

 130 |   constructor MkNSProvider

 131 |   provideNS : m Namespace

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

 135 |   provideNS = lift provideNS

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

 139 | inNS ns = MkNSProvider $ pure ns

 143 | NoNS : Monad m => NamespaceProvider m

 144 | NoNS = inNS (MkNS [])

 146 | inGenNSImpl : Namespace -> Name -> Name -> Name

 147 | inGenNSImpl (MkNS strs) p n = do

 148 |   let newNS =

 149 |     case n of

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

 151 |         n => []

 152 |   NS (MkNS $ newNS ++ show p :: strs) $ dropNS n

 155 | inGenNS : SpecTask -> Name -> Name

 156 | inGenNS task = inGenNSImpl task.currentNs task.resultName

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

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

 163 | applyArgAliases :

 164 |   (as : List Arg) ->

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

 166 |   List (Name, Name) ->

 167 |   SortedMap Name TTImp ->

 168 |   Subset (List Arg) (All IsNamedArg)

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

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

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

 172 |     case ys of

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

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

 175 |   let Element rec prec = applyArgAliases xs ys newIns

 176 |   Element

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

 178 |     (ItIsNamed :: prec)

 180 | prependS : String -> Name -> Name

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

 185 | transformArgNames :

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

 187 |   (as : List Arg) ->

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

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

 190 | transformArgNames f as = do

 191 |   let aliases = pushIn as %search <&> \(x `Element` xN) => (argName x, f $ Expr.argName x @{xN})

 192 |   (applyArgAliases as aliases empty, aliases)

 195 | hideExplicitArg : Arg -> Arg

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

 199 | makeImplicit : Arg -> Arg

 200 | makeImplicit = { piInfo := ImplicitArg }

 203 | makeTypeArgM0 : Arg -> Arg

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

 207 | tupleOfN : Nat -> TTImp -> TTImp

 208 | tupleOfN 0 _ = `(MkUnit)

 209 | tupleOfN 1 t = t

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

 213 | tupleOf : List TTImp -> TTImp

 214 | tupleOf [] = `(MkUnit)

 215 | tupleOf [x] = x

 216 | tupleOf (x :: xs) = `(MkPair ~x ~(tupleOf xs))

 219 | hideExplicitArgPreservesNames :

 220 |   (args : List Arg) ->

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

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

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

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

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

 226 |     ItIsNamed :: hideExplicitArgPreservesNames xs

 229 | makeImplicitPreservesNames :

 230 |   (args : List Arg) ->

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

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

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

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

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

 236 |     ItIsNamed :: makeImplicitPreservesNames xs

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

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

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

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

 252 | checkArgsUse : MonadError SpecialisationError m => List Arg -> SortedSet Name -> m ()

 253 | checkArgsUse [] _ = pure ()

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

 255 |   let Just n = x.name

 256 |   | _ => checkArgsUse xs t

 257 |   if contains n t

 258 |     then checkArgsUse xs t

 259 |     else throwError UnusedVarError

 262 | cleanupHoleAutoImplicitsImpl : TTImp -> TTImp

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

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

 265 | cleanupHoleAutoImplicitsImpl x = x

 269 | (.appWith) :

 270 |   (arg : Arg) ->

 271 |   (0 _ : IsNamedArg arg) =>

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

 273 |   (argValues : SortedMap Name TTImp) ->

 274 |   AnyApp

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

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

 280 | (.appsWith) :

 281 |   (args: List Arg) ->

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

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

 284 |   (argValues : SortedMap Name TTImp) ->

 285 |   List AnyApp

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

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

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

 292 | getTask :

 293 |   Monad m =>

 294 |   NamespaceProvider m =>

 295 |   MonadError SpecialisationError m =>

 296 |   NamesInfoInTypes =>

 297 |   (resultName : Name) ->

 298 |   (resultKind : TTImp) ->

 299 |   (resultContent : TTImp) ->

 300 |   m SpecTask

 301 | getTask resultName resultKind resultContent = do

 302 |   let (tqArgs, tqRet) = unLambda resultContent

 303 |   -- Check for unused arguments

 304 |   checkArgsUse tqArgs $ usesVariables tqRet

 305 |   -- Extract name of polymorphic type

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

 307 |   | _ => throwError TaskTypeExtractionError

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

 309 |   let Yes tqArgsNamed = all isNamedArg tqArgs

 310 |   | _ => throwError UnnamedArgInLambdaError

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

 312 |   let (Element tqArgs tqArgsNamed, tqAlias) = transformArgNames (prependS "fv^\{resultName}^") tqArgs

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

 314 |   let (ttArgs, _) = unPi resultKind

 315 |   -- Check for partial application in spec

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

 317 |   | _ => throwError PartialSpecError

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

 319 |   let Yes ttArgsNamed = all isNamedArg ttArgs

 320 |   | _ => throwError UnnamedArgInLambdaError

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

 322 |   let Element ttArgs ttArgsNamed = applyArgAliases ttArgs tqAlias empty

 323 |   -- Get current namespace

 324 |   currentNs <- provideNS

 325 |   -- Get polymorphic type's info

 326 |   let Just polyTy = lookupType typeName

 327 |   | _ => throwError $ MissingTypeInfoError typeName

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

 329 |   let Yes polyTyNamed = areAllTyArgsNamed polyTy

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

 331 |   let specInvocation = reAppAny

 332 |           (var (inGenNSImpl currentNs (snd $ unNS $ resultName) (snd $ unNS $ resultName))) $

 333 |             ttArgs.appsWith @{ttArgsNamed} var empty

 334 |   pure $ MkSpecTask

 335 |     { tqArgs

 336 |     , tqRet

 337 |     , tqArgsNamed

 338 |     , ttArgs

 339 |     , ttArgsNamed

 340 |     , currentNs

 341 |     , resultName = snd $ unNS resultName

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

 343 |     , specInvocation

 344 |     , polyTy

 345 |     , polyTyNamed

 346 |     }

 348 | namespace TypeInfoInvoke

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

 352 |   export

 353 |   (.apply) :

 354 |     (ti : TypeInfo) ->

 355 |     (0 tiN : AllTyArgsNamed ti) =>

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

 357 |     (argValues : SortedMap Name TTImp) ->

 358 |     TTImp

 359 |   (.apply) t f vals = do

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

 362 | namespace ConInvoke

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

 366 |   export

 367 |   (.apply) :

 368 |     (con : Con) ->

 369 |     (0 _ : ConArgsNamed con) =>

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

 371 |     (argValues : SortedMap Name TTImp) ->

 372 |     TTImp

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

 375 | namespace VectAll

 376 |   ||| Proof that Vect.All works over Vect.snoc

 377 |   export

 378 |   0 snoc: All p prev -> p new -> All p (Data.Vect.snoc prev new)

 379 |   snoc [] y = [y]

 380 |   snoc (y :: ys) z = y :: snoc ys z

 382 |   ||| List + List.All to Vect + Vect.All

 383 |   export

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

 385 |   fromListAll [] = Element [] []

 386 |   fromListAll (x :: xs) @{p :: ps} = do

 387 |     let Element xs' ps' = fromListAll xs @{ps}

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

 390 | namespace ListAll

 391 |   ||| Proof that List.All works over List.snoc

 392 |   export

 393 |   0 snoc : All p prev -> p new -> All p (Data.List.snoc prev new)

 394 |   snoc [] y = [y]

 395 |   snoc (y :: ys) z = y :: snoc ys z

 397 | namespace SnocListAll

 398 |   ||| SnocList + SnocList.All to List + List.All

 399 |   export

 400 |   toListAll : (sl : SnocList Arg) -> (0 _ : All p sl) -> Subset (List Arg) (All p)

 401 |   toListAll [<] [<] = Element [] []

 402 |   toListAll (sx :< x) (sy :< y) = do

 403 |     let Element xs ys = toListAll sx sy

 404 |     Element (snoc xs x) (snoc ys y)

 407 | record RecursionSearchState where

 408 |   constructor MkRSS

 409 |   ||| Accumulated transformation to cast from argument type to specialised type

 410 |   mToPRenames : SortedMap Name TTImp

 411 |   ||| Accumulated transformation to cast from specialised type to argument type

 412 |   pToMRenames : SortedMap Name TTImp

 413 |   ||| SnocList containing recursiveness of previous arguments

 414 |   areArgsRecursive : SnocList Bool

 415 |   ||| The pre-baked arguments to run unification with.

 416 |   argsForUnifier : Subset (Vect (length areArgsRecursive) Arg) (All IsNamedArg)

 417 |   ||| Accumulated arguments to be used in specialised constructor

 418 |   argsOutput : Subset (SnocList Arg) (All IsNamedArg)

 421 | record ArgMeta where

 422 |   constructor MkAMeta

 423 |   ||| The argument's type can be substituted by specialised type invocation

 424 |   isRecursiveArg : Bool

 427 | record ConMeta where

 428 |   constructor MkCMeta

 429 |   ||| Metadata for each argument

 430 |   argMeta : List ArgMeta

 431 |   ||| Replacements to transform original argument's type to specialised type

 432 |   mToPRenames : SortedMap Name TTImp

 433 |   ||| Replacement to transform specialised type to original argument's type

 434 |   pToMRenames : SortedMap Name TTImp

 436 | hasRecursiveArgs : ConMeta -> Bool

 437 | hasRecursiveArgs = any isRecursiveArg . argMeta

 439 | countRecursiveArgs : ConMeta -> Nat

 440 | countRecursiveArgs = count isRecursiveArg  . argMeta

 442 | recursiveArgNames : Con -> ConMeta -> List Name

 443 | recursiveArgNames con meta = do

 444 |   let recursiveArgPairs = List.filter (isRecursiveArg . snd) $ zip con.args meta.argMeta

 445 |   fromMaybe "" . name . fst <$> recursiveArgPairs

 448 | record TypeMeta where

 449 |   constructor MkTyMeta

 450 |   ||| Specialisation-related metadata for each constructor

 451 |   conMeta : List ConMeta

 455 | bindConRecArgsAliased : Con -> ConMeta -> (Name -> Name) -> TTImp

 456 | bindConRecArgsAliased con meta alias =

 457 |   reAppAny (var con.name) $ processArg <$> zip con.args meta.argMeta

 458 |   where

 459 |   maybeBind : Arg -> ArgMeta -> TTImp

 460 |   maybeBind a am = if isRecursiveArg am then bindVar $ alias $ fromMaybe "" a.name else `(_)

 462 |   processArg : (Arg, ArgMeta) -> AnyApp

 463 |   processArg (a@(MkArg _ ExplicitArg _ _), am) = PosApp $ maybeBind a am

 464 |   processArg (a, am) = NamedApp (fromMaybe "" a.name) $ maybeBind a am

 466 | parameters (t : SpecTask)

 467 |   ---------------------------

 468 |   --- CONSTRUCTOR MAPPING ---

 469 |   ---------------------------

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

 471 |   mapCons :

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

 473 |          (0 _ : ConArgsNamed pCon) =>

 474 |          r) ->

 475 |     List r

 476 |   mapCons f = do

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

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

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

 481 |   mapUCons :

 482 |     (f : UnificationResult ->

 483 |          (pCon : Con) ->

 484 |          (0 _ : ConArgsNamed pCon) =>

 485 |          Nat ->

 486 |          r) ->

 487 |     UniResults ->

 488 |     List r

 489 |   mapUCons f rs = do

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

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

 492 |         f' (Element con _ :: xs) (Success res :: ys) n = f res con n :: f' xs ys (S n)

 493 |         f' (_ :: xs)             (_ :: ys)           n = f' xs ys n

 494 |         f' _ _ _ = []

 495 |     f' adp rs 0

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

 498 |   map2UConsN :

 499 |     (f : UnificationResult ->

 500 |          (mt : TypeInfo) ->

 501 |          (0 _ : AllTyArgsNamed mt) =>

 502 |          (con : Con) ->

 503 |          (0 _ : ConArgsNamed con) =>

 504 |          (mcon : Con) ->

 505 |          (0 _ : ConArgsNamed mcon) =>

 506 |          ConMeta ->

 507 |          Nat ->

 508 |          r) ->

 509 |     UniResults ->

 510 |     (mt : TypeInfo) ->

 511 |     (0 _ : AllTyArgsNamed mt) =>

 512 |     TypeMeta ->

 513 |     List r

 514 |   map2UConsN f rs mt @{mtp} meta = do

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

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

 517 |     f' 0 p1 p2 rs meta.conMeta

 518 |     where

 519 |       f' :

 520 |         Nat ->

 521 |         List (Subset Con ConArgsNamed) ->

 522 |         List (Subset Con ConArgsNamed) ->

 523 |         UniResults ->

 524 |         List ConMeta ->

 525 |         List r

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

 527 |         f res mt con mcon meta' n :: f' (S n) xs ys zs metas

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

 529 |         f' n xs ys zs ms

 530 |       f' _ _ _ _ _ = []

 532 |   -------------------------------

 533 |   --- CONSTRUCTOR UNIFICATION ---

 534 |   -------------------------------

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

 537 |   unifyCon : MonadLog m => (unifier : CanUnify m) => (con : Con) -> (0 conN : ConArgsNamed con) => m UnificationVerdict

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

 539 |     let Element ca _ = fromListAll con.args @{conArgsNamed}

 540 |     let Element ta _ = fromListAll t.tqArgs @{t.tqArgsNamed}

 541 |     let uniTask =

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

 543 |                 {rfv=_} ta t.fullInvocation

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

 545 |     uniRes <- unify uniTask

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

 548 |   ---------------------------------

 549 |   --- SPECIFIED TYPE GENERATION ---

 550 |   ---------------------------------

 552 |   ||| Generate argument of a specified constructor

 553 |   mkSpecArg : (ur : UnificationResult) -> Fin (ur.uniDg.freeVars) -> Subset Arg IsNamedArg

 554 |   mkSpecArg ur fvId = do

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

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

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

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

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

 561 |   getVar : TTImp -> Maybe Name

 562 |   getVar (IVar _ n) = Just n

 563 |   getVar _ = Nothing

 565 |   ||| Check if a given argument is "recursive" (i.e. its type can be replaced with invocation of specialised type)

 566 |   checkArgRecursion :

 567 |     Monad m =>

 568 |     CanUnify m =>

 569 |     MonadLog m =>

 570 |     NamesInfoInTypes =>

 571 |     RecursionSearchState -> Subset Arg IsNamedArg -> m RecursionSearchState

 572 |   checkArgRecursion rss (Element thisArg thisArgNamed) = do

 573 |     let (MkRSS cRenames pToMRenames areArgsRec (Element argsForUni _) (Element argsOut _)) = rss

 574 |     let (aLhs, aa) = unAppAny thisArg.type

 575 |     let True = (length aa /= 0) || (isJust $ lookupType =<< getVar aLhs)

 576 |       | False => do

 577 |         let outPiInfo = substituteVariables cRenames <$> thisArg.piInfo

 578 |         let outType = substituteVariables cRenames thisArg.type

 579 |         let Element outArg outArgNamed =

 580 |             Element (MkArg thisArg.count outPiInfo (Just $ argName thisArg) outType) ItIsNamed

 581 |         pure $

 582 |           MkRSS

 583 |             cRenames

 584 |             pToMRenames

 585 |             (areArgsRec :< False)

 586 |             (Element (snoc argsForUni thisArg) (snoc %search thisArgNamed))

 587 |             (Element (argsOut :< outArg) (%search :< outArgNamed))

 588 |     let Element ta _ = fromListAll t.tqArgs @{t.tqArgsNamed}

 589 |     let uniTask = MkUniTask {lfv=_} argsForUni thisArg.type {rfv=_} ta t.fullInvocation

 590 |     ur <- unify uniTask

 591 |     case ur of

 592 |       Success ur => do

 593 |         let typeArgs = t.ttArgs.appsWith @{t.ttArgsNamed} var ur.fullResult

 594 |         logPoint DetailedDebug "specialiseData.fra" [] $ show ur.fullResult

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

 596 |         logPoint DetailedDebug "specialiseData.fra" [] $ show tyRet

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

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

 599 |         let outPiInfo = (\x => `(cast ~x)) . substituteVariables cRenames <$> thisArg.piInfo

 600 |         let outType = substituteVariables cRenames tyRet

 601 |         let Element outArg outArgNamed =

 602 |             Element (MkArg thisArg.count outPiInfo (Just $ argName thisArg) outType) ItIsNamed

 603 |         pure $

 604 |           MkRSS

 605 |             (insert (argName thisArg) `(~mToPImpl ~(var $ argName thisArg)) cRenames)

 606 |             (insert (argName thisArg) `(~pToMImpl ~(var $ argName thisArg)) pToMRenames)

 607 |             (areArgsRec :< True)

 608 |             (Element (snoc argsForUni thisArg) (snoc %search thisArgNamed))

 609 |             (Element (argsOut :< outArg) (%search :< outArgNamed))

 610 |       _ => do

 611 |         let outPiInfo = substituteVariables cRenames <$> thisArg.piInfo

 612 |         let outType = substituteVariables cRenames thisArg.type

 613 |         let Element outArg outArgNamed =

 614 |             Element (MkArg thisArg.count outPiInfo (Just $ argName thisArg) outType) ItIsNamed

 615 |         pure $

 616 |           MkRSS

 617 |             cRenames

 618 |             pToMRenames

 619 |             (areArgsRec :< False)

 620 |             (Element (snoc argsForUni thisArg) (snoc %search thisArgNamed))

 621 |             (Element (argsOut :< outArg) (%search :< outArgNamed))

 623 |   ||| Generate a specialised constructor

 624 |   mkSpecCon :

 625 |     Monad m =>

 626 |     CanUnify m =>

 627 |     MonadLog m =>

 628 |     NamesInfoInTypes =>

 629 |     (params : SpecialisationParams) =>

 630 |     (newArgs : List Arg) ->

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

 632 |     UnificationResult ->

 633 |     (con : Con) ->

 634 |     (0 _ : ConArgsNamed con) =>

 635 |     Nat ->

 636 |     m $ (Subset Con ConArgsNamed, ConMeta)

 637 |   mkSpecCon newArgs ur pCon cIdx = do

 638 |     let specArgs = mkSpecArg ur <$> ur.order

 639 |     let Element args allArgs =

 640 |       pullOut specArgs

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

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

 643 |     let n = if params.eraseConNames then fromString "\{t.resultName}^Con^\{show cIdx}" else dropNS pCon.name

 644 |     rssRhs <- foldlM checkArgRecursion (MkRSS empty empty [<] (Element [] []) (Element [<] [<])) specArgs

 645 |     let (MkRSS mToPRenames pToMRenames argsAreRecursive' _ (Element outArgs' outArgsNamed')) = rssRhs

 646 |     let Element outArgs outArgsNamed = toListAll outArgs' outArgsNamed'

 647 |     let conMeta = MkCMeta (MkAMeta <$> toList argsAreRecursive') mToPRenames pToMRenames

 648 |     pure $ (MkCon

 649 |       { name = inGenNS t $ n

 650 |       , args = outArgs

 651 |       , type = substituteVariables mToPRenames tyRet

 652 |       } `Element` TheyAreNamed outArgsNamed, conMeta)

 654 |   ||| Generate a specialised type

 655 |   mkSpecTy :

 656 |     Monad m => CanUnify m => MonadLog m =>

 657 |     SpecialisationParams => NamesInfoInTypes =>

 658 |     UniResults -> m $ (Subset TypeInfo AllTyArgsNamed, TypeMeta)

 659 |   mkSpecTy ur = do

 660 |     let 0 _ = t.ttArgsNamed

 661 |     let muc = mapUCons (mkSpecCon t.ttArgs) ur

 662 |     specConsMeta <- traverse id muc

 663 |     let (specCons, specMeta) = unzip specConsMeta

 664 |     let Element cons consAreNamed = pullOut specCons

 665 |     pure $ (MkTypeInfo

 666 |       { name = inGenNS t t.resultName

 667 |       , args = t.ttArgs

 668 |       , cons

 669 |       } `Element` TheyAllAreNamed t.ttArgsNamed consAreNamed, MkTyMeta specMeta)

 671 |   mkSpecTySig : Decl

 672 |   mkSpecTySig = iDataLater Public t.resultName (piAll type t.ttArgs)

 674 |   ------------------------

 675 |   --- CLAIM DERIVATION ---

 676 |   ------------------------

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

 678 |   forallMTArgs : TTImp -> TTImp

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

 681 |   applyMTArgs : TTImp -> TTImp

 682 |   applyMTArgs =

 683 |     flip (foldl (\x,arg => x .! (fromMaybe "" arg.name, var $ fromMaybe "" arg.name))) $

 684 |       makeTypeArgM0 . hideExplicitArg <$> t.ttArgs

 686 |   ||| Generate specialised to polimorphic type conversion function signature

 687 |   mkMToPImplClaim : Decl

 688 |   mkMToPImplClaim = public' "mToPImpl" $ forallMTArgs $ arg t.specInvocation .-> t.fullInvocation

 690 |   ||| Generate specialised to polimorphic cast signature

 691 |   mkMToPClaim : Decl

 692 |   mkMToPClaim = interfaceHint Public "mToP" $ forallMTArgs $ `(Cast ~(t.specInvocation) ~(t.fullInvocation))

 694 |   ||| Decidable equality signatures

 695 |   mkDecEqImplClaim : Decl

 696 |   mkDecEqImplClaim =

 697 |     let tInv = t.specInvocation

 698 |     in public' "decEqImpl" $ forallMTArgs $

 699 |       piAll

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

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

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

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

 704 |         ]

 706 |   mkDecEqClaim : Decl

 707 |   mkDecEqClaim = interfaceHint Public "decEq'" $ forallMTArgs `(DecEq ~(t.fullInvocation) => DecEq ~(t.specInvocation))

 709 |   mkShowClaims : List Decl

 710 |   mkShowClaims =

 711 |     [ public' "showImpl" $

 712 |       forallMTArgs

 713 |         `(Show ~(t.fullInvocation) => ~(t.specInvocation) -> String)

 714 |     , public' "showPrecImpl" $

 715 |       forallMTArgs

 716 |         `(Show ~(t.fullInvocation) => Prec -> ~(t.specInvocation) -> String)

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

 718 |       `(Show ~(t.fullInvocation) => Show ~(t.specInvocation))

 719 |     ]

 721 |   mkEqClaims : List Decl

 722 |   mkEqClaims = do

 723 |     let tInv = t.specInvocation

 724 |     [ public' "eqImpl" $ forallMTArgs

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

 726 |     , public' "neqImpl" $ forallMTArgs

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

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

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

 730 |     ]

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

 733 |   mkPToMImplClaim : Decl

 734 |   mkPToMImplClaim = public' "pToMImpl" $ forallMTArgs $ arg t.fullInvocation .-> t.specInvocation

 736 |   ||| Generate specialised to polimorphic cast signature

 737 |   mkPToMClaim : Decl

 738 |   mkPToMClaim =

 739 |     interfaceHint Public "pToM" $ forallMTArgs $ `(Cast ~(t.fullInvocation) ~(t.specInvocation))

 741 |   mkFromStringClaims : List Decl

 742 |   mkFromStringClaims = do

 743 |     let tInv = t.specInvocation

 744 |     [ public' "fromStringImpl" $

 745 |         forallMTArgs

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

 747 |     , interfaceHint Public "fromString'" $

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

 749 |     ]

 751 |   mkNumClaims : List Decl

 752 |   mkNumClaims = do

 753 |     let tInv = t.specInvocation

 754 |     [ public' "numImpl" $

 755 |         forallMTArgs

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

 757 |     , public' "plusImpl" $

 758 |         forallMTArgs

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

 760 |     , public' "starImpl" $

 761 |         forallMTArgs

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

 763 |     , interfaceHint Public "num'" $

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

 765 |     ]

 767 |   standardClaims : List Decl

 768 |   standardClaims =

 769 |     [ mkMToPImplClaim

 770 |     , mkMToPClaim

 771 |     , mkDecEqImplClaim

 772 |     , mkDecEqClaim

 773 |     ] ++ join

 774 |       [ mkShowClaims

 775 |       , mkEqClaims

 776 |       ]

 778 |   decidedClaims : List Decl

 779 |   decidedClaims =

 780 |     [ mkPToMImplClaim

 781 |     , mkPToMClaim

 782 |     ] ++ join

 783 |       [ mkFromStringClaims

 784 |       , mkNumClaims

 785 |       ]

 787 |   ------------------------------------

 788 |   --- POLY TO POLY CAST DERIVATION ---

 789 |   ------------------------------------

 791 |   transMachineVars : TTImp -> TTImp

 792 |   transMachineVars $ IVar fc n@(MN ns nn) = IVar fc $ fromString "MS^\{show ns}^\{show nn}"

 793 |   transMachineVars $ IBindVar fc n@(MN ns nn) = IBindVar fc $ fromString "MS^\{show ns}^\{show nn}"

 794 |   transMachineVars t = t

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

 799 |   mkMToPImplClause :

 800 |     UnificationResult ->

 801 |     (mt : TypeInfo) ->

 802 |     (0 _ : AllTyArgsNamed mt) =>

 803 |     (pCon : Con) ->

 804 |     (0 _ : ConArgsNamed pCon) =>

 805 |     (mCon : Con) ->

 806 |     (0 _ : ConArgsNamed mCon) =>

 807 |     ConMeta ->

 808 |     Nat ->

 809 |     Clause

 810 |   mkMToPImplClause ur _ con mcon meta _ =

 811 |     mapClause transMachineVars $

 812 |       var "mToPImpl" .$

 813 |         mcon.apply bindVar

 814 |           (substituteVariables

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

 816 |       .= (substituteVariables meta.mToPRenames $ con.apply var ur.fullResult)

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

 819 |   mkMToPImplDecls :

 820 |     UniResults ->

 821 |     (mt : TypeInfo) ->

 822 |     (0 _ : AllTyArgsNamed mt) =>

 823 |     TypeMeta ->

 824 |     List Decl

 825 |   mkMToPImplDecls urs mt meta = do

 826 |     let clauses = map2UConsN mkMToPImplClause urs mt meta

 827 |     [ def "mToPImpl" clauses

 828 |     ]

 830 |   ||| Generate specialised to polymorphic cast signature

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

 832 |   mkMToPSig mt = do

 833 |     forallMTArgs $ `(Cast ~(t.specInvocation) ~(t.fullInvocation))

 835 |   ||| Generate specialised to polymorphic cast declarations

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

 837 |   mkMToPDecls mt =

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

 839 |     ]

 841 |   -----------------------------------

 842 |   --- CAST INJECTIVITY DERIVATION ---

 843 |   -----------------------------------

 845 |   ||| Emit a recursive call to castInjImpl constructing the proof from given names

 846 |   recCastInj : Name -> Name -> TTImp

 847 |   recCastInj p1 p2 = `(~(var $ inGenNS t $ "castInjImpl") $ trans ~(var p1) $ sym ~(var p2))

 849 |   ||| Generate a with-clause corresponding to a single recursive argument

 850 |   mkArgWithClause : Name -> TTImp -> Clause -> Clause

 851 |   mkArgWithClause argName existingLhs inner = do

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

 853 |     let lhsArg = var $ fromString "lhs^\{argName}"

 854 |     let rhsArg = var $ fromString "rhs^\{argName}"

 855 |     let p1 = Just (MW, fromString "\{argName}^p1")

 856 |     let p2 = Just (MW, fromString "\{argName}^p2")

 857 |     withClause existingLhs MW `(~mToPImpl ~lhsArg) p1 [] [

 858 |       withClause `(~existingLhs | _) MW `(~mToPImpl ~rhsArg) p2 [] [inner]

 859 |     ]

 861 |   ||| Wrap a term into a number of `IAppWith`s with underscores

 862 |   withManyUnders : Nat -> TTImp -> TTImp

 863 |   withManyUnders 0 x = x

 864 |   withManyUnders (S n) x = withManyUnders n `(~x | _)

 866 |   ||| Generate a final with-clause that matches all equality proofs to `Refl`s

 867 |   mkFinalClause : (con : Con) -> (0 _ : ConArgsNamed con) => ConMeta -> Clause

 868 |   mkFinalClause con meta = do

 869 |     let emptyCon = con.apply (\_ => `(_)) empty

 870 |     let recArgAmount = countRecursiveArgs meta

 871 |     let initialLhs = withManyUnders (2 * recArgAmount) $

 872 |       var "castInjImpl" .! ("castInj^x", emptyCon) .! ("castInj^y", emptyCon) .$ var "Refl"

 873 |     let recNames = recursiveArgNames con meta

 874 |     let recFns = (\n => recCastInj (fromString "\{n}^p1") (fromString "\{n}^p2")) <$> recNames

 875 |     withClause initialLhs MW (tupleOf recFns) Nothing [] [

 876 |       `(~initialLhs | ~(tupleOfN recArgAmount `(Refl))) .= `(Refl)

 877 |     ]

 879 |   ||| Generate a left-hand-side for recursive argument with-clauses

 880 |   mkInitialLhs : Con -> ConMeta -> TTImp

 881 |   mkInitialLhs con meta = do

 882 |     let lhsCon = bindConRecArgsAliased con meta $ prependS "lhs^"

 883 |     let rhsCon = bindConRecArgsAliased con meta $ prependS "rhs^"

 884 |     var "castInjImpl" .! ("castInj^x", lhsCon) .! ("castInj^y", rhsCon) .$ bindVar "prf"

 886 |   ||| Wrap a clause in with-clauses for all given names

 887 |   mkRecArgClauses : List Name -> TTImp -> Clause -> Clause

 888 |   mkRecArgClauses [] exLhs inner = inner

 889 |   mkRecArgClauses (x :: xs) exLhs inner = mkArgWithClause x exLhs $ mkRecArgClauses xs `(~exLhs | _ | _) inner

 891 |   ||| Derive a single cast injectivity clause

 892 |   mkCastInjClause :

 893 |     UnificationResult ->

 894 |     (mt : TypeInfo) ->

 895 |     (0 _ : AllTyArgsNamed mt) =>

 896 |     (con : Con) ->

 897 |     (0 cn : ConArgsNamed con) =>

 898 |     (mcon : Con) ->

 899 |     (0 mcn : ConArgsNamed mcon) =>

 900 |     ConMeta ->

 901 |     Nat ->

 902 |     Clause

 903 |   mkCastInjClause ur mt _ con meta n = do

 904 |     if not (hasRecursiveArgs meta)

 905 |       then do

 906 |         let emptyCon = con.apply (\_ => `(_)) empty

 907 |         (var "castInjImpl") .! ("castInj^x", emptyCon) .! ("castInj^y", emptyCon) .$ `(Refl) .= `(Refl)

 908 |       else do

 909 |         let finalClause = mkFinalClause con meta

 910 |         let recNames = recursiveArgNames con meta

 911 |         let initLhs = mkInitialLhs con meta

 912 |         mkRecArgClauses recNames initLhs finalClause

 914 |   ||| Derive cast injectivity proof

 915 |   mkCastInjDecls :

 916 |     UniResults ->

 917 |     (mt : TypeInfo) ->

 918 |     (0 mtp : AllTyArgsNamed mt) =>

 919 |     TypeMeta ->

 920 |     List Decl

 921 |   mkCastInjDecls ur ti meta = do

 922 |     let xVar = "castInj^x"

 923 |     let yVar = "castInj^y"

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

 925 |     let mToPImplVar = applyMTArgs $ var $ inGenNS t "mToPImpl"

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

 927 |                 ti.apply var empty

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

 929 |                 ti.apply var empty

 930 |     let eqs =

 931 |       `((~(mToPImplVar .$ var xVar)

 932 |           ~=~

 933 |           ~(mToPImplVar .$ var yVar)) ->

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

 935 |     let castInjImplClauses = map2UConsN mkCastInjClause ur ti meta

 936 |     [ claim M0 Public [] "castInjImpl" $ forallMTArgs $ pi arg1 $ pi arg2 $ eqs

 937 |     , def "castInjImpl" castInjImplClauses

 938 |     , claim M0 Public [Hint False] "castInj" $ forallMTArgs $

 939 |         `(Injective ~(mToPImplVar))

 940 |     , def "castInj" $ singleton $

 941 |         `(castInj) .= `(MkInjective castInjImpl)

 942 |     ]

 944 |   -------------------------------------

 945 |   --- DECIDABLE EQUALITY DERIVATION ---

 946 |   -------------------------------------

 948 |   ||| Decidable equality clause

 949 |   mkDecEqImplClause : Clause

 950 |   mkDecEqImplClause =

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

 952 |     in `(decEqImpl x1 x2)

 953 |         .=

 954 |         `(decEqInj {f = ~mToPImpl} $

 955 |           let x1' : ~(t.fullInvocation);

 956 |               x1' = (~mToPImpl x1);

 957 |               x2' : ~(t.fullInvocation);

 958 |               x2' = (~mToPImpl x2);

 959 |           in decEq x1' x2')

 961 |   ||| Derive decidable equality

 962 |   mkDecEqDecls :

 963 |     UniResults ->

 964 |     (mt : TypeInfo) ->

 965 |     (0 _ : AllTyArgsNamed mt) =>

 966 |     List Decl

 967 |   mkDecEqDecls _ ti = do

 968 |     [ def "decEqImpl" [ mkDecEqImplClause ]

 969 |     , def "decEq'"

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

 971 |     ]

 973 |   -----------------------

 974 |   --- SHOW DERIVATION ---

 975 |   -----------------------

 977 |   ||| Derive Show implementation via cast

 978 |   mkShowDecls :

 979 |     UniResults ->

 980 |     (mt : TypeInfo) ->

 981 |     (0 _ : AllTyArgsNamed mt) =>

 982 |     List Decl

 983 |   mkShowDecls _ ti = do

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

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

 986 |     , def "showPrecImpl"

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

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

 989 |     ]

 991 |   ---------------------

 992 |   --- EQ DERIVATION ---

 993 |   ---------------------

 995 |   ||| Derive Eq implementation via cast

 996 |   mkEqDecls :

 997 |     UniResults ->

 998 |     (mt : TypeInfo) ->

 999 |     (0 _ : AllTyArgsNamed mt) =>

1000 |     List Decl

1001 |   mkEqDecls _ ti = do

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

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

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

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

1006 |     ]

1008 |   ------------------------------------

1009 |   --- POLY TO POLY CAST DERIVATION ---

1010 |   ------------------------------------

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

1013 |   mkPToMImplSig :

1014 |     UniResults ->

1015 |     (mt : TypeInfo) ->

1016 |     (0 _ : AllTyArgsNamed mt) =>

1017 |     TTImp

1018 |   mkPToMImplSig _ mt =

1019 |     forallMTArgs $ arg t.fullInvocation .-> t.specInvocation

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

1023 |   mkPToMImplClause :

1024 |     UnificationResult ->

1025 |     (mt : TypeInfo) ->

1026 |     (0 _ : AllTyArgsNamed mt) =>

1027 |     (pCon : Con) ->

1028 |     (0 _ : ConArgsNamed pCon) =>

1029 |     (mCon : Con) ->

1030 |     (0 _ : ConArgsNamed mCon) =>

1031 |     ConMeta ->

1032 |     Nat ->

1033 |     Clause

1034 |   mkPToMImplClause ur _ con mcon meta _ =

1035 |     mapClause transMachineVars $

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

1037 |         (substituteVariables

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

1039 |       .= (substituteVariables meta.pToMRenames $ mcon.apply var ur.fullResult)

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

1042 |   mkPToMImplDecls :

1043 |     UniResults ->

1044 |     (mt : TypeInfo) ->

1045 |     (0 _ : AllTyArgsNamed mt) =>

1046 |     TypeMeta ->

1047 |     List Decl

1048 |   mkPToMImplDecls urs mt meta = do

1049 |     let clauses = map2UConsN mkPToMImplClause urs mt meta

1050 |     [ def "pToMImpl" clauses

1051 |     ]

1053 |   ||| Generate specialised to polymorphic cast signature

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

1055 |   mkPToMSig mt = do

1056 |     forallMTArgs $ `(Cast ~(t.fullInvocation) ~(t.specInvocation))

1058 |   ||| Generate specialised to polymorphic cast declarations

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

1060 |   mkPToMDecls mt =

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

1062 |     ]

1064 |   -----------------------------

1065 |   --- FROMSTRING DERIVATION ---

1066 |   -----------------------------

1068 |   mkFromStringDecls :

1069 |     (mt : TypeInfo) ->

1070 |     (0 _ : AllTyArgsNamed mt) =>

1071 |     List Decl

1072 |   mkFromStringDecls ti = do

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

1074 |     [ def "fromStringImpl"

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

1076 |     , def "fromString'"

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

1078 |     ]

1080 |   ----------------------

1081 |   --- NUM DERIVATION ---

1082 |   ----------------------

1084 |   mkNumDecls :

1085 |     (mt : TypeInfo) ->

1086 |     (0 _ : AllTyArgsNamed mt) =>

1087 |     List Decl

1088 |   mkNumDecls ti = do

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

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

1091 |     [ def "numImpl"

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

1093 |     , def "plusImpl"

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

1095 |     , def "starImpl"

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

1097 |     , def "num'"

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

1099 |             `(MkNum

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

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

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

1103 |         ]

1104 |     ]

1106 |   ------------------------------------

1107 |   --- SPECIALISED TYPE DECLARATION ---

1108 |   ------------------------------------

1110 |   (.declNoNS) : TypeInfo -> Decl

1111 |   (.declNoNS) ti =

1112 |     iData Public tyName tySig [] conITys

1113 |     where

1114 |       tyName = snd $ unNS ti.name

1115 |       tySig = piAll type ti.args

1116 |       conITys = (.iTy) <$> ti.cons

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

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

1120 |   specDecls uniResults specTy specMeta = do

1121 |     let specTySig = mkSpecTySig

1122 |     let specTyDecl = specTy.declNoNS

1123 |     logPoint DetailedDebug "specialiseData.specDecls.specTy.sig" [specTy] $ show mkSpecTySig

1124 |     logPoint DetailedDebug "specialiseData.specDecls.specTy" [specTy] $ show specTyDecl

1125 |     let mToPImplClaim = mkMToPImplClaim

1126 |     let mToPImplDecls = mkMToPImplDecls uniResults specTy specMeta

1127 |     logPoint DetailedDebug "specialiseData.specDecls.mToPImpl.sig" [specTy] $ show mToPImplClaim

1128 |     logPoint DetailedDebug "specialiseData.specDecls.mToPImpl" [specTy] $ show mToPImplDecls

1129 |     let mToPClaim = mkMToPClaim

1130 |     let mToPDecls = mkMToPDecls specTy

1131 |     logPoint DetailedDebug "specialiseData.specDecls.mToP.sig" [specTy] $ show mToPClaim

1132 |     logPoint DetailedDebug "specialiseData.specDecls.mToP" [specTy] $ show mToPDecls

1133 |     let castInjDecls = mkCastInjDecls uniResults specTy specMeta

1134 |     logPoint DetailedDebug "specialiseData.specDecls.castInj" [specTy] $ show castInjDecls

1135 |     let decEqClaims : List Decl = [ mkDecEqImplClaim, mkDecEqClaim ]

1136 |     let decEqDecls = mkDecEqDecls uniResults specTy

1137 |     logPoint DetailedDebug "specialiseData.specDecls.decEq.sig" [specTy] $ show decEqClaims

1138 |     logPoint DetailedDebug "specialiseData.specDecls.decEq" [specTy] $ show decEqDecls

1139 |     let showClaims = mkShowClaims

1140 |     let showDecls = mkShowDecls uniResults specTy

1141 |     logPoint DetailedDebug "specialiseData.specDecls.show.sig" [specTy] $ show showClaims

1142 |     logPoint DetailedDebug "specialiseData.specDecls.show" [specTy] $ show showDecls

1143 |     let eqClaims = mkEqClaims

1144 |     let eqDecls = mkEqDecls uniResults specTy

1145 |     logPoint DetailedDebug "specialiseData.specDecls.eq.sig" [specTy] $ show eqClaims

1146 |     logPoint DetailedDebug "specialiseData.specDecls.eq" [specTy] $ show eqDecls

1147 |     let pToMImplClaim = mkPToMImplClaim

1148 |     let pToMImplDecls = mkPToMImplDecls uniResults specTy specMeta

1149 |     logPoint DetailedDebug "specialiseData.specDecls.pToMImpl.sig" [specTy] $ show pToMImplClaim

1150 |     logPoint DetailedDebug "specialiseData.specDecls.pToMImpl" [specTy] $ show pToMImplDecls

1151 |     let pToMClaim = mkPToMClaim

1152 |     let pToMDecls = mkPToMDecls specTy

1153 |     logPoint DetailedDebug "specialiseData.specDecls.pToM.sig" [specTy] $ show pToMClaim

1154 |     logPoint DetailedDebug "specialiseData.specDecls.pToM" [specTy] $ show pToMDecls

1155 |     let fromStringClaims = mkFromStringClaims