
   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 Data.Vect.Quantifiers
   8 | import Decidable.Equality
   9 | import Deriving.Show
  10 | import Language.Reflection
  11 | import Language.Reflection.Compat
  12 | import Language.Reflection.Expr
  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 | export %hint
  41 | sUT : Show UnificationTask
  42 | sUT = %runElab derive
  43 | 
  44 | ||| Free variable output data
  45 | public export
  46 | record FVData where
  47 |   constructor MkFVData
  48 |   ||| Free variable name
  49 |   name : Name
  50 |   ||| Free variable hole name
  51 |   holeName : String
  52 |   ||| Free variable count
  53 |   rig : Count
  54 |   ||| Free variable PiInfo
  55 |   piInfo : PiInfo TTImp
  56 |   ||| Free variable type
  57 |   type : TTImp
  58 |   ||| Free variable value
  59 |   value : Maybe TTImp
  60 | 
  61 | %name FVData fv, fvData
  62 | 
  63 | export %hint
  64 | sFVData : Show FVData
  65 | sFVData = %runElab derive
  66 | 
  67 | export
  68 | Eq FVData where
  69 |   (MkFVData name holeName rig piInfo type value) == (MkFVData name' holeName' rig' piInfo' type' value') =
  70 |     name == name' && holeName == holeName' && rig == rig' && piInfo == piInfo' && type == type' && value == value'
  71 | 
  72 | export
  73 | Interpolation FVData where
  74 |   interpolate (MkFVData n h r p t v) = concat {t=List} [ showPiInfo p $ showCount r "\{n} \{h} : \{show t}", " = \{show v}" ]
  75 | 
  76 | ||| Make FVData out of most its components and an argument
  77 | export
  78 | makeFVData : (String, Arg, Name, TTImp, Maybe TTImp) -> FVData
  79 | makeFVData (h, fv, n, t, v) = MkFVData n h fv.count fv.piInfo t v
  80 | 
  81 | public export
  82 | record FVDeps (freeVars : Nat) where
  83 |   constructor MkFVDeps
  84 |   typeDeps : FinSet freeVars
  85 |   valueDeps : FinSet freeVars
  86 |   piInfoDeps : FinSet freeVars
  87 | 
  88 | %name FVDeps deps
  89 | 
  90 | {freeVars : Nat} -> Show (FVDeps freeVars) where
  91 |   showPrec p t =
  92 |     showCon p "MkFVDeps" $
  93 |       concat {t=List} $
  94 |         [ showArg t.typeDeps
  95 |         , showArg t.valueDeps
  96 |         , showArg t.piInfoDeps
  97 |         ]
  98 | 
  99 | {freeVars : Nat} -> Eq (FVDeps freeVars) where
 100 |   (==) a b = a.typeDeps == b.typeDeps && a.valueDeps == b.valueDeps && a.piInfoDeps == b.piInfoDeps
 101 | 
 102 | export
 103 | mergeDeps : FVDeps fv -> FinSet fv
 104 | mergeDeps (MkFVDeps typeDeps valueDeps piInfoDeps) = union typeDeps $ union valueDeps piInfoDeps
 105 | 
 106 | export
 107 | removeDeps : FinSet fv -> FVDeps fv -> FVDeps fv
 108 | removeDeps d =
 109 |   { typeDeps $= flip difference d
 110 |   , valueDeps $= flip difference d
 111 |   , piInfoDeps $= flip difference d
 112 |   }
 113 | 
 114 | ||| Free variable depenfdency graph
 115 | public export
 116 | record DependencyGraph where
 117 |   constructor MkDG
 118 |   ||| Free variable amount
 119 |   freeVars : Nat
 120 |   ||| Free variable data
 121 |   fvData : Vect freeVars FVData
 122 |   ||| Free variable dependency matrix
 123 |   fvDeps : Vect freeVars $ FVDeps freeVars
 124 |   ||| The set of all i: (Fin freeVars), where (index i fvData).value = None
 125 |   empties : FinSet freeVars
 126 |   ||| For all i : (Fin freeVars); (lookup (index i fvData).name nameToId) = i
 127 |   nameToId : SortedMap Name $ Fin freeVars
 128 |   ||| For all i : (Fin freeVars); (lookup (index i fvData).holeName holeToId) = i
 129 |   holeToId : SortedMap String $ Fin freeVars
 130 | 
 131 | %name DependencyGraph dg, depGraph
 132 | 
 133 | -- Implemented by hand due to idris-lang/Idris2#3838
 134 | export
 135 | Show DependencyGraph where
 136 |   showPrec p t =
 137 |     showCon p "MkDG" $
 138 |       concat {t=List} $
 139 |         [ showArg t.freeVars
 140 |         , showArg t.fvData
 141 |         , showArg t.fvDeps
 142 |         , showArg t.empties
 143 |         , showArg t.nameToId
 144 |         , showArg t.holeToId
 145 |         ]
 146 | 
 147 | export
 148 | Eq DependencyGraph where
 149 |   (==) (MkDG a b c d e f) (MkDG a' b' c' d' e' f') with (decEq a a')
 150 |    (==) (MkDG a b c d e f) (MkDG a b' c' d' e' f') | Yes Refl =
 151 |     b == b' && c == c' && d == d' && e == e' && f == f'
 152 |    _                                               | No _ = False
 153 | 
 154 | ||| Unification result
 155 | public export
 156 | record UnificationResult where
 157 |   constructor MkUR
 158 |   ||| Task given to the unifier
 159 |   task : UnificationTask
 160 |   ||| Dependency graph returned by the unifier
 161 |   uniDg : DependencyGraph
 162 |   ||| LHS free variable (polymorphic constructor argument) values
 163 |   lhsResult : SortedMap Name TTImp
 164 |   ||| RHS free variable (specialised type argument) values
 165 |   rhsResult : SortedMap Name TTImp
 166 |   ||| All free variable values
 167 |   fullResult : SortedMap Name TTImp
 168 |   ||| Order of dependency of free variables without values
 169 |   ||| (specialised constructor arguments)
 170 |   order : List $ Fin uniDg.freeVars
 171 | 
 172 | -- Implemented by hand due to idris-lang/Idris2#3838
 173 | export
 174 | Show UnificationResult where
 175 |   showPrec p t =
 176 |     showCon p "MkUR" $
 177 |       concat {t=List} $
 178 |         [ showArg t.task
 179 |         , showArg t.uniDg
 180 |         , showArg t.lhsResult
 181 |         , showArg t.rhsResult
 182 |         , showArg t.fullResult
 183 |         , showArg t.order
 184 |         ]
 185 | 
 186 | public export
 187 | data UnificationError : Type where
 188 |   CatastrophicError : UnificationError
 189 |   InternalError : String -> UnificationError
 190 |   TargetTypeError : TTImp -> UnificationError
 191 |   ExtractionError : TTImp -> UnificationError
 192 |   NoUnificationError : UnificationError
 193 | 
 194 | export %hint
 195 | sUE : Show UnificationError
 196 | sUE = %runElab derive
 197 | 
 198 | export
 199 | Eq UnificationError where
 200 |   CatastrophicError == CatastrophicError = True
 201 |   InternalError s == InternalError s' = s == s'
 202 |   TargetTypeError t == TargetTypeError t' = t == t'
 203 |   ExtractionError t == ExtractionError t' = t == t'
 204 |   NoUnificationError == NoUnificationError = True
 205 |   _ == _ = False
 206 | 
 207 | public export
 208 | data UnificationVerdict : Type where
 209 |   Success : UnificationResult -> UnificationVerdict
 210 |   Undecided : UnificationVerdict
 211 |   Fail : UnificationError -> UnificationVerdict
 212 | 
 213 | export %hint
 214 | sUV : Show UnificationVerdict
 215 | sUV = %runElab derive
 216 | 
 217 | export %inline
 218 | isSuccess : UnificationVerdict -> Bool
 219 | isSuccess (Success _) = True
 220 | isSuccess _ = False
 221 | 
 222 | export %inline
 223 | isUndecided : UnificationVerdict -> Bool
 224 | isUndecided Undecided = True
 225 | isUndecided _ = False
 226 | 
 227 | export %inline
 228 | isFail : UnificationVerdict -> Bool
 229 | isFail (Fail _) = True
 230 | isFail _ = False
 231 | 
 232 | export
 233 | Cast (Either (Maybe UnificationError) UnificationResult) UnificationVerdict where
 234 |   cast (Right s) = Success s
 235 |   cast (Left Nothing) = Undecided
 236 |   cast (Left $ Just e) = Fail e
 237 | 
 238 | public export
 239 | interface CanUnify (0 m : Type -> Type) where
 240 |   constructor MkCanUnify
 241 |   unify : UnificationTask -> m UnificationVerdict
 242 | 
 243 | export
 244 | Monad m => MonadTrans t => CanUnify m => CanUnify (t m) where
 245 |   unify = lift . unify
 246 | 
 247 | ||| List all free variables that don't depende on any other free variables
 248 | leaves : (dg : DependencyGraph) -> FinSet dg.freeVars
 249 | leaves dg =
 250 |   foldl
 251 |     (\acc,(id, deps) => if null deps then insert id acc else acc)
 252 |     empty $
 253 |   zip (allFins dg.freeVars) (map mergeDeps dg.fvDeps)
 254 | 
 255 | ||| List all the free variables without a value that don't depend on any other free variables
 256 | emptyLeaves : (dg : DependencyGraph) -> FinSet dg.freeVars
 257 | emptyLeaves dg = intersection dg.empties $ leaves dg
 258 | 
 259 | ||| List all the free variables without a value in order of dependency
 260 | |||
 261 | ||| The function is monadic due to over-normalisation during elaborator script execution causing bad derivator performance
 262 | flattenEmpties : Monad m => (dg : DependencyGraph) -> m $ SnocList $ Fin dg.freeVars
 263 | flattenEmpties dg = flattenEmpties' dg [<]
 264 |   where
 265 |     flattenEmpties' : (dg : DependencyGraph) -> SnocList (Fin dg.freeVars) -> m $ SnocList $ Fin dg.freeVars
 266 |     flattenEmpties' dg@(MkDG {freeVars, fvData, fvDeps, empties, nameToId, holeToId}) ctx = do
 267 |       els <- pure $ id $ emptyLeaves dg
 268 |       let False = null els
 269 |       | _ => pure ctx
 270 |       -- Now els is a non-empty subset of dg.empties
 271 |       flattenEmpties'
 272 |         -- `assert_smaller dg` is a workaround for a non-working `assert_smaller empties`
 273 |         (assert_smaller dg $ MkDG
 274 |           freeVars
 275 |           fvData
 276 |           (removeDeps els <$> fvDeps)
 277 |           (assert_smaller empties $ flip difference els empties)
 278 |           nameToId
 279 |           holeToId)
 280 |         (ctx <>< toList els)
 281 | 
 282 | ||| Find all variables which have no value
 283 | filterEmpty : Vect _ FVData -> List (Name, TTImp)
 284 | filterEmpty = foldl myfun []
 285 |   where
 286 |     myfun : List (Name, TTImp) -> FVData -> List (Name, TTImp)
 287 |     myfun xs x =
 288 |       case x.value of
 289 |         Just val => (x.name, val) :: xs
 290 |         Nothing => xs
 291 | 
 292 | ||| Calculate UnificationResult (var-to-value mappings and empty leaf dependency order)
 293 | |||
 294 | ||| The function is monadic due to over-normalisation during elaborator script execution causing bad derivator performance
 295 | export
 296 | finalizeDG : Monad m => (task : UnificationTask) -> (dg : DependencyGraph) -> m UnificationResult
 297 | finalizeDG task dg = do
 298 |   fvOrder <- flattenEmpties dg
 299 |   urList <- pure $ id $ filterEmpty dg.fvData
 300 |   (lhsRL, rhsRL) <- pure $ id $ List.splitAt task.lfv urList
 301 |   pure $ MkUR
 302 |     { task
 303 |     , uniDg = dg
 304 |     , lhsResult = fromList lhsRL
 305 |     , rhsResult = fromList rhsRL
 306 |     , fullResult = fromList urList
 307 |     , order = toList fvOrder
 308 |     }
 309 |