0 | module Deriving.DepTyCheck.Util.DeepConsApp
  1 |
  2 | import public Control.Monad.Writer.Interface
  3 |
  4 | import public Data.Fin.Split
  5 | import public Data.List.Ex
  6 | import public Data.List.Map
  7 | import public Data.List.Set
  8 | import public Data.SortedSet
  9 | import public Data.Vect.Ex
 10 |
 11 | import public Language.Reflection.Compat.TypeInfo
 12 |
 13 | import Deriving.Show
 14 |
 15 | %default total
 16 | %language ElabReflection
 17 |
 18 | public export
 19 | data ConsDetermInfo = DeterminedByType | NotDeterminedByType | MustDecEqWith TTImp
 20 |
 21 | export %hint
 22 | ShowConsDetermInfo : Show ConsDetermInfo
 23 | ShowConsDetermInfo = %runElab derive
 24 |
 25 | export
 26 | Cast Bool ConsDetermInfo where
 27 |   cast True  = DeterminedByType
 28 |   cast False = NotDeterminedByType
 29 |
 30 | export
 31 | Cast ConsDetermInfo Bool where
 32 |   cast DeterminedByType    = True
 33 |   cast NotDeterminedByType = False
 34 |   cast $ MustDecEqWith {}  = False
 35 |
 36 | public export
 37 | determineMustDecEqs : ConsDetermInfo -> ConsDetermInfo
 38 | determineMustDecEqs DeterminedByType    = DeterminedByType
 39 | determineMustDecEqs NotDeterminedByType = NotDeterminedByType
 40 | determineMustDecEqs $ MustDecEqWith {}  = DeterminedByType
 41 |
 42 | export
 43 | Semigroup ConsDetermInfo where
 44 |   x@(MustDecEqWith {}) <+> MustDecEqWith {} = x
 45 |   MustDecEqWith {} <+> DeterminedByType = DeterminedByType
 46 |   DeterminedByType <+> MustDecEqWith {} = DeterminedByType
 47 |   DeterminedByType <+> DeterminedByType = DeterminedByType
 48 |   NotDeterminedByType <+> x = x
 49 |   x <+> NotDeterminedByType = x
 50 |
 51 | export
 52 | Monoid ConsDetermInfo where
 53 |   neutral = NotDeterminedByType
 54 |
 55 | public export
 56 | BindExprFun : Nat -> Type
 57 | BindExprFun n = (bindExpr : Fin n -> TTImp) -> {-bind expression-} TTImp
 58 |
 59 | public export
 60 | DeepConsAnalysisRes : (collectConsDetermInfo : Bool) -> Type
 61 | DeepConsAnalysisRes False = List Name
 62 | DeepConsAnalysisRes True = (appliedFreeNames : List (Name, ConsDetermInfo) ** BindExprFun appliedFreeNames.length)
 63 |
 64 | MaybeConsDetermInfo : Bool -> Type
 65 | MaybeConsDetermInfo True  = ConsDetermInfo
 66 | MaybeConsDetermInfo False = Unit
 67 |
 68 | ||| Analyses whether the given expression can be an expression of free variables applied (maybe deeply) to a number of data constructors.
 69 | |||
 70 | ||| Returns which of given free names are actually used in the given expression, in order of appearance in the expression.
 71 | ||| Notice that applied free names may repeat as soon as one name is used several times in the given expression.
 72 | |||
 73 | ||| Also, a function returning a bind expression (an expression replacing all free names with bind names (`IBindVar`))
 74 | ||| is also returned.
 75 | ||| This function requires bind variable names as input.
 76 | ||| It returns correct bind expression only when all given bind names are different.
 77 | export
 78 | analyseDeepConsApp : NamesInfoInTypes =>
 79 |                      MonadWriter (List String) m =>
 80 |                      (collectConsDetermInfo : Bool) ->
 81 |                      (freeNames : SortedSet Name) ->
 82 |                      (analysedExpr : TTImp) ->
 83 |                      m $ DeepConsAnalysisRes collectConsDetermInfo
 84 | analyseDeepConsApp ccdi freeNames = pass . map (, nub) . isD where
 85 |
 86 |   isD : TTImp -> m $ DeepConsAnalysisRes ccdi
 87 |   isD e = do
 88 |
 89 |     -- Treat given expression as a function application to some name
 90 |     let (IVar _ lhsName, args) = unAppAny e
 91 |       | (IType {}   , _) => pure $ noFree e
 92 |       | (IPrimVal {}, _) => pure $ noFree e
 93 |       | _ => bad "not an application to a variable"
 94 |
 95 |     -- Check if this is a free name
 96 |     let False = contains lhsName freeNames && null args
 97 |       | True => pure $ if ccdi then ([(lhsName, neutral)] ** \f => f FZ) else [lhsName]
 98 |
 99 |     -- Check that this is an application to a constructor's name
100 |     let Just (conArgs, conType) = lookupCon lhsName <&> \con => (con.args, con.type)
101 |       | Nothing => pure $ if ccdi then ([(MN (show e) 0, MustDecEqWith e)] ** \f => f FZ) else []
102 |
103 |     -- Acquire type-determination info, if needed
104 |     typeDetermInfo : Vect conArgs.length $ MaybeConsDetermInfo ccdi <-
105 |       if ccdi then assert_total {- `ccdi` is `True` here when `False` inside -} $ typeDeterminedArgs conArgs conType else pure neutral
106 |
107 |     let Just typeDetermInfo = reorder typeDetermInfo
108 |       | Nothing => bad "INTERNAL ERROR: cannot reorder formal determ info along with a call to a constructor"
109 |
110 |     -- Analyze deeply all the arguments
111 |     deepArgs <- for (args.asVect `zip` typeDetermInfo) $
112 |       \(anyApp, typeDetermined) => do
113 |         subResult <- isD $ assert_smaller e $ getExpr anyApp
114 |         let subResult = if ccdi then mapSnd (<+> typeDetermined) `mapLstDPair` subResult else subResult
115 |         pure (anyApp, subResult)
116 |
117 |     -- Collect all the applied names and form proper application expression with binding variables
118 |     pure $ foldl (mergeApp _) (noFree $ var lhsName) deepArgs
119 |
120 |     where
121 |       noFree : TTImp -> DeepConsAnalysisRes ccdi
122 |       noFree e = if ccdi then ([] ** const e) else []
123 |
124 |       bad : String -> m $ DeepConsAnalysisRes ccdi
125 |       bad msg = tell [msg] $> noFree implicitTrue
126 |         -- well, returning `implicitTrue` may be too kinda lazy, maybe, we should return `e` itself, maybe dotted;
127 |         -- but we need to work with variables determination correctly -- they mustn't be deceqed further down
128 |
129 |       mergeApp : (ccdi : _) -> DeepConsAnalysisRes ccdi -> (AnyApp, DeepConsAnalysisRes ccdi) -> DeepConsAnalysisRes ccdi
130 |       mergeApp False namesL (_, namesR) = namesL ++ namesR
131 |       mergeApp True (namesL ** bindL) (anyApp, (namesR ** bindR)) = MkDPair (namesL ++ namesR) $ \bindNames => do
132 |         let bindNames : Fin (namesL.length + namesR.length) -> _ := rewrite sym $ lengthConcat namesL namesR in bindNames
133 |         let lhs = bindL $ bindNames . indexSum . Left
134 |         let rhs = bindR $ bindNames . indexSum . Right
135 |         reAppAny1 lhs $ const rhs `mapExpr` anyApp
136 |
137 |       mapLstDPair : (a -> b) -> (x : List a ** BindExprFun x.length) -> (x : List b ** BindExprFun x.length)
138 |       mapLstDPair f (lst ** d) = (map f lst ** rewrite lengthMap {f} lst in d)
139 |
140 |       ||| Determines which constructor's arguments would be definitely determined by fully known result type.
141 |       typeDeterminedArgs : (args : List Arg) -> (type : TTImp) -> m $ Vect args.length ConsDetermInfo
142 |       typeDeterminedArgs args type = do
143 |         let conArgNames = fromList $ mapI args $ \idx, arg => (argName' arg, idx)
144 |         determined <- analyseDeepConsApp False (SortedSet.keySet conArgNames) type
145 |         let determined = mapMaybe (lookup' conArgNames) determined
146 |         pure $ map cast $ presenceVect $ fromList determined
147 |
148 |       reorder : {formalArgs : List Arg} -> {apps : List AnyApp} -> Vect formalArgs.length a -> Maybe $ Vect apps.length a
149 |       reorder xs = reorder' (fromList formalArgs `zip` xs) apps where
150 |         reorder' : Vect n (Arg, a) -> (apps : List AnyApp) -> Maybe $ Vect apps.length a
151 |         reorder' xs        []      = if isJust $ find ((== ExplicitArg) . piInfo . fst) xs
152 |                                        then Nothing {- not all explicit parameters are used -} else Just []
153 |         reorder' []        (_::_)  = Nothing
154 |         reorder' xs@(_::_) (a::as) = do
155 |           let searchFun : Arg -> Bool
156 |               searchFun = case a of
157 |                             PosApp _      => (== ExplicitArg) . piInfo
158 |                             NamedApp nm _ => \na => isImplicit na.piInfo && na.name == Just nm
159 |                             AutoApp _     => (== AutoImplicit) . piInfo
160 |                             WithApp _     => const False
161 |           let Just i = findIndex (searchFun . fst) xs
162 |             | Nothing => Nothing
163 |           let restxs = deleteAt i xs
164 |           (snd (index i xs) ::) <$> reorder' restxs as
165 |