
   0 | module Deriving.SpecialiseData.TaskFormation
   1 | 
   2 | import public Language.Reflection
   3 | import public Language.Reflection.Syntax
   4 | import public Language.Reflection.Compat.TypeInfo
   5 | import public Language.Reflection.Logging -- workaround for idris-lang/Idris2#2439
   6 | 
   7 | allQImpl : Monad m => NamesInfoInTypes => TTImp -> TTImp -> m TTImp
   8 | allQImpl (IPi {}) r = pure r
   9 | allQImpl (IApp {}) (IApp _ (Implicit {}) _) = pure `(?)
  10 | allQImpl (IApp {}) r@(IApp {}) = pure r
  11 | allQImpl (IApp {}) _ = pure `(?)
  12 | allQImpl v@(IVar _ n) _ =
  13 |   case lookupType n of
  14 |     Just _ => pure v
  15 |     Nothing => pure `(?)
  16 | allQImpl _ _ = pure `(?)
  17 | 
  18 | ||| Replace every non-function sub-expression with a question mark
  19 | |||
  20 | ||| (x -> (y -> z) -> q) becomes (? -> (? -> ?) -> ?)
  21 | allQuestions : NamesInfoInTypes => TTImp -> TTImp
  22 | allQuestions t = runIdentity $ mapMTTImp' allQImpl t
  23 | 
  24 | ||| Information about a generator's argument extracted from GenSignature
  25 | public export
  26 | record GenArg where
  27 |   constructor MkGenArg
  28 |   ||| Formal argument beloging to a type constructor
  29 |   arg : Arg
  30 |   ||| Value of the actual/given argument (if present)
  31 |   given : Maybe TTImp
  32 | 
  33 | export
  34 | LogPosition GenArg where
  35 |   logPosition (MkGenArg a Nothing) = "\{fromMaybe "<unnamed arg>" a.name}"
  36 |   logPosition (MkGenArg a $ Just t) = "(\{fromMaybe "<unnamed arg>" a.name} := \{show t})"
  37 | 
  38 | unGA : List GenArg -> (List Arg, List (Maybe TTImp))
  39 | unGA [] = ([], [])
  40 | unGA (x :: xs) = let (ys, zs) = unGA xs in (x.arg :: ys, x.given :: zs)
  41 | 
  42 | (.isGenerated) : GenArg -> Bool
  43 | (.isGenerated) = isNothing . given
  44 | 
  45 | (.isGiven) : GenArg -> Bool
  46 | (.isGiven) = isJust . given
  47 | 
  48 | singleArg : NamesInfoInTypes => Nat -> GenArg -> (TTImp, List GenArg)
  49 | singleArg n (MkGenArg a v) = do
  50 |   let n : Name = fromString "lam^\{show n}"
  51 |   (IVar EmptyFC n, [MkGenArg (MkArg a.count a.piInfo (Just n) $ allQuestions a.type) v])
  52 | 
  53 | public export
  54 | data ArgDecision = Passthrough | SpecLit TTImp | SpecRec Name (List GenArg)
  55 | 
  56 | isPassthrough : ArgDecision -> Bool
  57 | isPassthrough Passthrough = True
  58 | isPassthrough _ = False
  59 | 
  60 | export
  61 | specDecideArg : NamesInfoInTypes => GenArg -> (ArgDecision, String)
  62 | specDecideArg ga with (ga.given)
  63 |   specDecideArg ga | Nothing = (Passthrough, "No given value")
  64 |   specDecideArg ga | Just x = do
  65 |     let (appLhs, appTerms) = unAppAny x
  66 |     let IVar _ tyName = appLhs
  67 |       | IPrimVal _ (PrT _) => (SpecLit x, "Given a primitive type invocation")
  68 |       | _ => (Passthrough, "Given value head is not a variable")
  69 |     case lookupType tyName of
  70 |       Just tyInfo => case appTerms of
  71 |         [] => (SpecLit x, "Given a type invocation w/o arguments")
  72 |         _ => do
  73 |           let givens = map (uncurry MkGenArg) $ zip tyInfo.args $ popArgVals tyInfo.args (mkAllApps appTerms)
  74 |           (SpecRec tyName givens, "Given a type invocation")
  75 |       Nothing =>
  76 |         ( Passthrough
  77 |         , if (snd (unPi ga.arg.type) == `(Type))
  78 |             then "Given a non-global type expr"
  79 |             else "Given a non-type expr")
  80 | 
  81 | processArg :
  82 |   MonadLog m =>
  83 |   NamesInfoInTypes =>
  84 |   (GenArg -> (ArgDecision, String)) ->
  85 |   Name ->
  86 |   Nat ->
  87 |   GenArg ->
  88 |   m (TTImp, List GenArg)
  89 | 
  90 | processArgs :
  91 |   MonadLog m =>
  92 |   NamesInfoInTypes =>
  93 |   (GenArg -> (ArgDecision, String)) ->
  94 |   Name ->
  95 |   Nat ->
  96 |   List GenArg ->
  97 |   m (List AnyApp, List GenArg)
  98 | processArgs dec tyName k [] = pure ([], [])
  99 | processArgs dec tyName k (x :: xs) = do
 100 |   (aT, l) <- assert_total $ processArg dec tyName k x
 101 |   (recAA, l') <- processArgs dec tyName (k + length l) xs
 102 |   pure (appArg x.arg aT :: recAA, l ++ l')
 103 | 
 104 | processArg dec tyName argIdx ga =
 105 |   case dec ga of
 106 |     (Passthrough, s) =>
 107 |       logValue DetailedDebug "specialiseData.taskFormation" [tyName, ga]
 108 |         "\{s}, passing through" $ singleArg argIdx ga
 109 |     (SpecLit x, s) =>
 110 |       logValue DetailedDebug "specialiseData.taskFormation" [tyName, ga]
 111 |         "\{s}, specialising" (x, [])
 112 |     (SpecRec n givens, s) => do
 113 |       logPoint DetailedDebug "specialiseData.taskFormation" [tyName, ga]
 114 |         "\{s}, traversing arguments: \{show $ map (fromMaybe "" . name . arg) givens}"
 115 |       map (mapFst $ reAppAny (IVar EmptyFC n)) $ processArgs dec n argIdx $ takeWhile (.isGiven) givens
 116 | 
 117 | export
 118 | argsToSpecTask :
 119 |   MonadLog m =>
 120 |   NamesInfoInTypes =>
 121 |   (GenArg -> (ArgDecision, String)) ->
 122 |   Name ->
 123 |   List GenArg ->
 124 |   m (TTImp, List Arg, List $ Maybe TTImp)
 125 | argsToSpecTask dec tyName ga = bimap (reAppAny $ IVar EmptyFC tyName) unGA <$> processArgs dec tyName 0 ga
 126 | 
 127 | allAppsToGenArgs : List Arg -> AllApps -> List GenArg
 128 | allAppsToGenArgs [] aa = []
 129 | allAppsToGenArgs (x :: xs) aa = do
 130 |   let pav = popArgVal x aa
 131 |   let mr = fst <$> pav
 132 |   let aa = fromMaybe aa $ snd <$> pav
 133 |   MkGenArg x mr :: allAppsToGenArgs xs aa
 134 | 
 135 | export
 136 | exprToSpecTask :
 137 |   MonadLog m =>
 138 |   NamesInfoInTypes =>
 139 |   (GenArg -> (ArgDecision, String)) ->
 140 |   TTImp ->
 141 |   m $ Maybe (TTImp, List Arg, List $ Maybe TTImp)
 142 | exprToSpecTask dec expr = do
 143 |   let (appHead, appTerms) = unAppAny expr
 144 |   let (IVar _ tyName) = appHead
 145 |     | _ => logValue DetailedDebug "specialiseData.taskFormation" []
 146 |               "Head of expression is not a variable: \{show appHead}"
 147 |               Nothing
 148 |   let (Just tyInfo) = lookupType tyName
 149 |     | _ => logValue DetailedDebug "specialiseData.taskFormation" []
 150 |               "\{tyName} is not a global type"
 151 |               Nothing
 152 |   let allApps = mkAllApps appTerms
 153 |   let genArgs = allAppsToGenArgs tyInfo.args allApps
 154 |   let False = all isPassthrough $ fst . dec <$> genArgs
 155 |     | True => logValue DetailedDebug "specialiseData.taskFormation" []
 156 |                 "No non-passthrough arguments!"
 157 |                 Nothing
 158 |   Just <$> argsToSpecTask dec tyName genArgs
 159 |