0 | module Language.Reflection.Compat.TypeInfo
  1 |
  2 | import Data.List.Map
  3 | import Data.List.Set
  4 | import Data.SortedMap
  5 | import Data.SortedSet
  6 |
  7 | import public Language.Reflection.Compat.Constr
  8 | import public Language.Reflection.Expr
  9 |
 10 | import public Syntax.IHateParens.SortedSet
 11 |
 12 | %default total
 13 |
 14 | --------------------------------------------------------
 15 | --- Acquiring special representations from type info ---
 16 | --------------------------------------------------------
 17 |
 18 | ||| Returns a type constructor as `Con` by given type
 19 | typeCon : TypeInfo -> Con
 20 | typeCon ti = MkCon ti.name ti.args type
 21 |
 22 | ||| Generate a declaration from TypeInfo
 23 | export
 24 | (.decl) : TypeInfo -> Decl
 25 | (.decl) ti =
 26 |   iData Public ti.name tySig [] conITys
 27 |   where
 28 |     tySig = piAll type ti.args
 29 |     conITys = (.iTy) <$> ti.cons
 30 |
 31 | ---------------------------
 32 | --- Analysing type info ---
 33 | ---------------------------
 34 |
 35 | -- Returns a list without duplications
 36 | export
 37 | allInvolvedTypes : Elaboration m => (minimalRig : Count) -> TypeInfo -> m $ List TypeInfo
 38 | allInvolvedTypes minimalRig ti = toList <$> go [ti] empty where
 39 |   go : (left : List TypeInfo) -> (curr : SortedMap Name TypeInfo) -> m $ SortedMap Name TypeInfo
 40 |   go left curr = do
 41 |     let (c::left) = filter (not . isJust . lookup' curr . name) left
 42 |       | [] => pure curr
 43 |     let next = insert c.name c curr
 44 |     args <- atRig M0 $ join <$> for c.args typesOfArg
 45 |     cons <- join <$> for c.tyCons typesOfCon
 46 |     assert_total $ go (args ++ cons ++ left) next
 47 |     where
 48 |       atRig : Count -> m (List a) -> m (List a)
 49 |       atRig rig act = if rig >= minimalRig then act else pure []
 50 |
 51 |       typesOfExpr : TTImp -> m $ List TypeInfo
 52 |       typesOfExpr expr = map (mapMaybe id) $ for (allVarNames expr) $ catch . getInfo'
 53 |
 54 |       typesOfArg : Arg -> m $ List TypeInfo
 55 |       typesOfArg arg = atRig arg.count $ typesOfExpr arg.type
 56 |
 57 |       typesOfCon : Con -> m $ List TypeInfo
 58 |       typesOfCon con = [| atRig M0 (typesOfExpr con.type) ++ (join <$> for con.args typesOfArg) |]
 59 |
 60 | -- Fails if the given type info does not have all type args named
 61 | export
 62 | ensureTyArgsNamed : Elaboration m => (ty : TypeInfo) -> m $ AllTyArgsNamed ty
 63 | ensureTyArgsNamed ty = do
 64 |   let Yes prf = areAllTyArgsNamed ty
 65 |     | No _ => fail "Type info for type `\{ty.name}` contains unnamed arguments"
 66 |   pure prf
 67 |
 68 | export
 69 | (.argNames) : (ti : TypeInfo) -> (0 tiN : AllTyArgsNamed ti) => List Name
 70 | (.argNames) ti = argNames ti.args @{tiN.tyArgsNamed}
 71 |
 72 | --------------------------
 73 | --- Changing type info ---
 74 | --------------------------
 75 |
 76 | normaliseCons : Elaboration m => TypeInfo -> m TypeInfo
 77 | normaliseCons ty = for ty.cons normaliseCon <&> \cons' => {cons := cons'} ty
 78 |
 79 | ---------------------------
 80 | --- Names info in types ---
 81 | ---------------------------
 82 |
 83 | export
 84 | record NamesInfoInTypes where
 85 |   constructor Names
 86 |   types : ListMap Name TypeInfo
 87 |   cons  : ListMap Name (TypeInfo, Con)
 88 |   namesInTypes : ListMap TypeInfo $ SortedSet Name
 89 |
 90 | lookupByType : NamesInfoInTypes => Name -> Maybe $ SortedSet Name
 91 | lookupByType @{tyi} = lookup' tyi.types >=> lookup' tyi.namesInTypes
 92 |
 93 | lookupByCon : NamesInfoInTypes => Name -> Maybe $ SortedSet Name
 94 | lookupByCon @{tyi} = concatMap @{Deep} lookupByType . Prelude.toList . concatMap allVarNames' . conSubexprs . snd <=< lookup' tyi.cons
 95 |
 96 | typeByCon : NamesInfoInTypes => Con -> Maybe TypeInfo
 97 | typeByCon @{tyi} = map fst . lookup' tyi.cons . name
 98 |
 99 | export
100 | lookupType : NamesInfoInTypes => Name -> Maybe TypeInfo
101 | lookupType @{tyi} = lookup' tyi.types
102 |
103 | export
104 | lookupCon : NamesInfoInTypes => Name -> Maybe Con
105 | lookupCon @{tyi} n = snd <$> lookup n tyi.cons
106 |                  <|> typeCon <$> lookup n tyi.types
107 |
108 | export
109 | knownTypes : NamesInfoInTypes => ListMap Name TypeInfo
110 | knownTypes @{tyi} = tyi.types
111 |
112 | ||| Returns either resolved expression, or a non-unique name and the set of alternatives.
113 | -- We could use `Validated (SortedMap Name $ SortedSet Name) TTImp` as the result, if we depended on `contrib`.
114 | -- NOTICE: this function does not resolve re-export aliases, say, it does not resolve `Prelude.Nil` to `Prelude.Basics.Nil`.
115 | export
116 | resolveNamesUniquely : NamesInfoInTypes => (freeNames : SortedSet Name) -> TTImp -> Either (Name, SortedSet Name) TTImp
117 | resolveNamesUniquely @{tyi} freeNames = do
118 |   let allConsideredNames = keySet tyi.types `union` keySet tyi.cons
119 |   let reverseNamesMap = concatMap (uncurry SortedMap.singleton) $ allConsideredNames.asList >>= \n => allNameSuffixes n <&> (, SortedSet.singleton n)
120 |   mapATTImp' $ \case
121 |     v@(IVar fc n) => if contains n freeNames then id else do
122 |                        let Just resolvedAlts = lookup n reverseNamesMap | Nothing => id
123 |                        let [resolved] = Prelude.toList resolvedAlts
124 |                          | _ => const $ Left (n, resolvedAlts)
125 |                        const $ pure $ IVar fc resolved
126 |     _ => id
127 |
128 | export
129 | [TypeInfoEqByName] Eq TypeInfo where
130 |   (==) = (==) `on` name
131 |
132 | export
133 | [TypeInfoOrdByName] Ord TypeInfo using TypeInfoEqByName where
134 |   compare = comparing name
135 |
136 | export
137 | Semigroup NamesInfoInTypes where
138 |   Names ts cs nit <+> Names ts' cs' nit' = Names (ts `mergeLeft` ts') (cs `mergeLeft` cs') (nit <+> nit')
139 |
140 | Monoid NamesInfoInTypes where
141 |   neutral = let _ = TypeInfoEqByName
142 |              in Names empty empty empty
143 |
144 | export
145 | hasNameInsideDeep : NamesInfoInTypes => Name -> TTImp -> Bool
146 | hasNameInsideDeep @{tyi} nm = hasInside empty . allVarNames where
147 |
148 |   hasInside : (visited : SortedSet Name) -> (toLook : List Name) -> Bool
149 |   hasInside visited []           = False
150 |   hasInside visited (curr::rest) = if curr == nm then True else do
151 |     let new = if contains curr visited then [] else maybe [] Prelude.toList $ lookupByType curr
152 |     -- visited is limited and either growing or `new` is empty, thus `toLook` is strictly less
153 |     assert_total $ hasInside (insert curr visited) (new ++ rest)
154 |
155 | export
156 | isRecursive : NamesInfoInTypes => (con : Con) -> {default Nothing containingType : Maybe TypeInfo} -> Bool
157 | isRecursive con = case the (Maybe TypeInfo) $ containingType <|> typeByCon con of
158 |   Just containingType => any (hasNameInsideDeep containingType.name) $ conSubexprs con
159 |   Nothing             => False
160 |
161 | -- returns `Nothing` if given name is not a constructor
162 | export
163 | isRecursiveConstructor : NamesInfoInTypes => Name -> Maybe Bool
164 | isRecursiveConstructor @{tyi} n = lookup' tyi.cons n <&> \(ty, con) => isRecursive {containingType=Just ty} con
165 |
166 | export
167 | enrichNamesInfoInTypes : Elaboration m => List TypeInfo -> NamesInfoInTypes -> m NamesInfoInTypes
168 | enrichNamesInfoInTypes []         tyi = pure tyi
169 | enrichNamesInfoInTypes (ti::rest) tyi = do
170 |   ti <- normaliseCons ti
171 |   let subes = concatMap allVarNames' $ subexprs ti
172 |   new <- map join $ for (Prelude.toList subes) $ \n =>
173 |            if isNothing $ lookupByType n
174 |              then map toList $ catch $ getInfo' n
175 |              else pure []
176 |   let next = { types $= insert ti.name ti
177 |              , namesInTypes $= insert ti subes
178 |              , cons $= mergeLeft $ fromList $ ti.cons <&> \con => (con.name, ti, con)
179 |              } tyi
180 |   assert_total $ enrichNamesInfoInTypes (new ++ rest) next
181 |   where
182 |     subexprs : TypeInfo -> List TTImp
183 |     subexprs ty = map type ty.args ++ (ty.cons >>= conSubexprs)
184 |
185 | export
186 | getNamesInfoInTypes : Elaboration m => TypeInfo -> m NamesInfoInTypes
187 | getNamesInfoInTypes ty = enrichNamesInfoInTypes [ty] neutral
188 |
189 | export
190 | getNamesInfoInTypes' : Elaboration m => TTImp -> m NamesInfoInTypes
191 | getNamesInfoInTypes' expr = do
192 |   let varsFirstOrder = allVarNames expr
193 |   varsSecondOrder <- map concat $ for varsFirstOrder $ \n => do
194 |                        ns <- getType n
195 |                        pure $ SortedSet.insert n $ flip concatMap ns $ \(n', ty) => insert n' $ allVarNames' ty
196 |   tys <- map (mapMaybe id) $ for (Prelude.toList varsSecondOrder) $ catch . getInfo'
197 |   concat <$> Prelude.for tys getNamesInfoInTypes
198 |