0 | module Language.Reflection.Unify.Interface
  1 |
  2 | import Control.Monad.Either
  3 | import Data.Either
  4 | import Data.Fin.Set
  5 | import Data.SortedMap
  6 | import Data.Vect
  7 | import Decidable.Equality
  8 | import Derive.Prelude
  9 | import Language.Reflection
 10 | import Language.Reflection.Expr
 11 | import Language.Reflection.TTImp
 12 | import Language.Reflection.TT
 13 | import Language.Reflection.Syntax
 14 |
 15 | %language ElabReflection
 16 |
 17 | %default total
 18 |
 19 | ||| Unification task
 20 | public export
 21 | record UnificationTask where
 22 |   constructor MkUniTask
 23 |   ||| Amount of left-hand-side free variables
 24 |   {lfv : Nat}
 25 |   ||| Left-hand-side free variables
 26 |   lhsFreeVars : Vect lfv Arg
 27 |   {auto 0 lhsAreNamed : All IsNamedArg lhsFreeVars}
 28 |   ||| Left-hand-side expression
 29 |   lhsExpr : TTImp
 30 |   ||| Amount of right-hand-side free variables
 31 |   {rfv : Nat}
 32 |   ||| Right-hand-side free variables
 33 |   rhsFreeVars : Vect rfv Arg
 34 |   {auto 0 rhsAreNamed : All IsNamedArg rhsFreeVars}
 35 |   ||| Right-hand-side expression
 36 |   rhsExpr : TTImp
 37 |
 38 | %name UnificationTask task
 39 |
 40 | %runElab derive "Count" [Show]
 41 | %runElab derive "PiInfo" [Show]
 42 | %runElab derive "Syntax.Arg" [Show]
 43 |
 44 | export
 45 | Show UnificationTask where
 46 |   showPrec p t =
 47 |     showCon p "MkUniTask" $
 48 |       joinBy "" $
 49 |         [ showArg t.lfv
 50 |         , showArg t.lhsFreeVars
 51 |         , showArg t.lhsExpr
 52 |         , showArg t.rfv
 53 |         , showArg t.rhsFreeVars
 54 |         , showArg t.rhsExpr
 55 |         ]
 56 |
 57 | ||| Free variable output data
 58 | public export
 59 | record FVData where
 60 |   constructor MkFVData
 61 |   ||| Free variable name
 62 |   name : Name
 63 |   ||| Free variable hole name
 64 |   holeName : String
 65 |   ||| Free variable count
 66 |   rig : Count
 67 |   ||| Free variable PiInfo
 68 |   piInfo : PiInfo TTImp
 69 |   ||| Free variable type
 70 |   type : TTImp
 71 |   ||| Free variable value
 72 |   value : Maybe TTImp
 73 |
 74 | %name FVData fv, fvData
 75 |
 76 | %runElab derive "FVData" [Show, Eq]
 77 |
 78 | export
 79 | Interpolation FVData where
 80 |   interpolate (MkFVData n h r p t v) = joinBy "" [ showPiInfo p $ showCount r "\{n} \{h} : \{show t}", " = \{show v}" ]
 81 |
 82 | ||| Make FVData out of most its components and an argument
 83 | export
 84 | makeFVData : (String, Arg, Name, TTImp, Maybe TTImp) -> FVData
 85 | makeFVData (h, fv, n, t, v) = MkFVData n h fv.count fv.piInfo t v
 86 |
 87 | public export
 88 | record FVDeps (freeVars : Nat) where
 89 |   constructor MkFVDeps
 90 |   typeDeps : FinSet freeVars
 91 |   valueDeps : FinSet freeVars
 92 |   piInfoDeps : FinSet freeVars
 93 |
 94 | %name FVDeps deps
 95 |
 96 | {freeVars : Nat} -> Show (FVDeps freeVars) where
 97 |   showPrec p t =
 98 |     showCon p "MkFVDeps" $
 99 |       joinBy "" $
100 |         [ showArg t.typeDeps
101 |         , showArg t.valueDeps
102 |         , showArg t.piInfoDeps
103 |         ]
104 |
105 | {freeVars : Nat} -> Eq (FVDeps freeVars) where
106 |   (==) a b = a.typeDeps == b.typeDeps && a.valueDeps == b.valueDeps && a.piInfoDeps == b.piInfoDeps
107 |
108 | export
109 | mergeDeps : FVDeps fv -> FinSet fv
110 | mergeDeps (MkFVDeps typeDeps valueDeps piInfoDeps) = union typeDeps $ union valueDeps piInfoDeps
111 |
112 | export
113 | removeDeps : FinSet fv -> FVDeps fv -> FVDeps fv
114 | removeDeps d =
115 |   { typeDeps $= flip difference d
116 |   , valueDeps $= flip difference d
117 |   , piInfoDeps $= flip difference d
118 |   }
119 |
120 | ||| Free variable depenfdency graph
121 | public export
122 | record DependencyGraph where
123 |   constructor MkDG
124 |   ||| Free variable amount
125 |   freeVars : Nat
126 |   ||| Free variable data
127 |   fvData : Vect freeVars FVData
128 |   ||| Free variable dependency matrix
129 |   fvDeps : Vect freeVars $ FVDeps freeVars
130 |   ||| The set of all i: (Fin freeVars), where (index i fvData).value = None
131 |   empties : FinSet freeVars
132 |   ||| For all i : (Fin freeVars); (lookup (index i fvData).name nameToId) = i
133 |   nameToId : SortedMap Name $ Fin freeVars
134 |   ||| For all i : (Fin freeVars); (lookup (index i fvData).holeName holeToId) = i
135 |   holeToId : SortedMap String $ Fin freeVars
136 |
137 | %name DependencyGraph dg, depGraph
138 |
139 | %runElab derive "DependencyGraph" [Show]
140 |
141 | export
142 | Eq DependencyGraph where
143 |   (==) (MkDG a b c d e f) (MkDG a' b' c' d' e' f') with (decEq a a')
144 |    (==) (MkDG a b c d e f) (MkDG a b' c' d' e' f') | Yes Refl =
145 |     b == b' && c == c' && d == d' && e == e' && f == f'
146 |    _                                               | No _ = False
147 |
148 | ||| Unification result
149 | public export
150 | record UnificationResult where
151 |   constructor MkUR
152 |   ||| Task given to the unifier
153 |   task : UnificationTask
154 |   ||| Dependency graph returned by the unifier
155 |   uniDg : DependencyGraph
156 |   ||| LHS free variable (polymorphic constructor argument) values
157 |   lhsResult : SortedMap Name TTImp
158 |   ||| RHS free variable (specialised type argument) values
159 |   rhsResult : SortedMap Name TTImp
160 |   ||| All free variable values
161 |   fullResult : SortedMap Name TTImp
162 |   ||| Order of dependency of free variables without values
163 |   ||| (specialised constructor arguments)
164 |   order : List $ Fin uniDg.freeVars
165 |
166 | %runElab derive "UnificationResult" [Show]
167 |
168 | public export
169 | data UnificationError : Type where
170 |   CatastrophicError : UnificationError
171 |   InternalError : String -> UnificationError
172 |   TargetTypeError : TTImp -> UnificationError
173 |   ExtractionError : TTImp -> UnificationError
174 |   NoUnificationError : UnificationError
175 |
176 | %runElab derive "UnificationError" [Show, Eq]
177 |
178 | public export
179 | data UnificationVerdict : Type where
180 |   Success : UnificationResult -> UnificationVerdict
181 |   Undecided : UnificationVerdict
182 |   Fail : UnificationError -> UnificationVerdict
183 |
184 | %runElab derive "UnificationVerdict" [Show]
185 |
186 | export %inline
187 | isSuccess : UnificationVerdict -> Bool
188 | isSuccess (Success _) = True
189 | isSuccess _ = False
190 |
191 | export %inline
192 | isUndecided : UnificationVerdict -> Bool
193 | isUndecided Undecided = True
194 | isUndecided _ = False
195 |
196 | export %inline
197 | isFail : UnificationVerdict -> Bool
198 | isFail (Fail _) = True
199 | isFail _ = False
200 |
201 | export
202 | Cast (Either (Maybe UnificationError) UnificationResult) UnificationVerdict where
203 |   cast (Right s) = Success s
204 |   cast (Left Nothing) = Undecided
205 |   cast (Left $ Just e) = Fail e
206 |
207 | public export
208 | interface CanUnify (0 m : Type -> Type) where
209 |   constructor MkCanUnify
210 |   unify : UnificationTask -> m UnificationVerdict
211 |
212 | export
213 | Monad m => MonadTrans t => CanUnify m => CanUnify (t m) where
214 |   unify = lift . unify
215 |
216 | ||| List all free variables that don't depende on any other free variables
217 | leaves : (dg : DependencyGraph) -> FinSet dg.freeVars
218 | leaves dg =
219 |   foldl
220 |     (\acc,(id, deps) => if null deps then insert id acc else acc)
221 |     empty $
222 |   zip (allFins dg.freeVars) (map mergeDeps dg.fvDeps)
223 |
224 | ||| List all the free variables without a value that don't depend on any other free variables
225 | emptyLeaves : (dg : DependencyGraph) -> FinSet dg.freeVars
226 | emptyLeaves dg = intersection dg.empties $ leaves dg
227 |
228 | ||| List all the free variables without a value in order of dependency
229 | flattenEmpties : (dg : DependencyGraph) -> SnocList $ Fin dg.freeVars
230 | flattenEmpties dg = flattenEmpties' dg [<]
231 |   where
232 |     flattenEmpties' : (dg : DependencyGraph) -> SnocList (Fin dg.freeVars) -> SnocList $ Fin dg.freeVars
233 |     flattenEmpties' dg@(MkDG {freeVars, fvData, fvDeps, empties, nameToId, holeToId}) ctx = do
234 |       let els = emptyLeaves dg
235 |       let False = null els
236 |       | _ => ctx
237 |       -- Now els is a non-empty subset of dg.empties
238 |       flattenEmpties'
239 |         -- `assert_smaller dg` is a workaround for a non-working `assert_smaller empties`
240 |         (assert_smaller dg $ MkDG
241 |           freeVars
242 |           fvData
243 |           (removeDeps els <$> fvDeps)
244 |           (assert_smaller empties $ flip difference els empties)
245 |           nameToId
246 |           holeToId)
247 |         (ctx <>< toList els)
248 |
249 | ||| Find all variables which have no value
250 | filterEmpty : Vect _ FVData -> List (Name, TTImp)
251 | filterEmpty = foldl myfun []
252 |   where
253 |     myfun : List (Name, TTImp) -> FVData -> List (Name, TTImp)
254 |     myfun xs x =
255 |       case x.value of
256 |         Just val => (x.name, val) :: xs
257 |         Nothing => xs
258 |
259 | ||| Calculate UnificationResult (var-to-value mappings and empty leaf dependency order)
260 | export
261 | finalizeDG : (task : UnificationTask) -> (dg : DependencyGraph) -> UnificationResult
262 | finalizeDG task dg = do
263 |   let fvOrder = flattenEmpties dg
264 |   let urList = filterEmpty dg.fvData
265 |   let (lhsRL, rhsRL) = List.splitAt task.lfv urList
266 |   MkUR
267 |     { task
268 |     , uniDg = dg
269 |     , lhsResult = fromList lhsRL
270 |     , rhsResult = fromList rhsRL
271 |     , fullResult = fromList urList
272 |     , order = toList fvOrder
273 |     }
274 |