File tree Expand file tree Collapse file tree 1 file changed +20
-4
lines changed Expand file tree Collapse file tree 1 file changed +20
-4
lines changed Original file line number Diff line number Diff line change @@ -252,15 +252,31 @@ namespace MultiConnection
252252 mOrElse (Just x) _ = x
253253
254254 public export
255- mtype : (sv : SVObjList) -> FinsList (sv.length) -> Maybe SVObject
256- mtype sv [] = Nothing
257- mtype sv (f :: fs) = Just $ unpOrDefault $ typeOf sv f
255+ mtype : SVObjList -> Maybe SVObject
256+ mtype [] = Nothing
257+ mtype (s :: _ ) = Just $ unpOrDefault s
258+
259+ public export
260+ types : (sv : SVObjList) -> FinsList (sv.length) -> SVObjList
261+ types sv [] = []
262+ types sv (f :: fs) = typeOf sv f :: types sv fs
263+
264+ public export
265+ findUnpNet : SVObjList -> Maybe SVObject
266+ findUnpNet [] = Nothing
267+ findUnpNet (s :: sv) = if isUnpacked s && isMD s then Just s else findUnpNet sv
268+
269+ public export
270+ resolveConnType : {ms : _} -> {m : _} -> {subMs : _} ->
271+ (ssk : FinsList $ subSnks' ms m subMs) -> (ssc : FinsList $ subSrcs' ms m subMs) -> SVObject
272+ resolveConnType ssk ssc = let allSubPorts = types (subSnks ms m subMs) ssk ++ types (subSrcs ms m subMs) ssc in
273+ mOrElse (findUnpNet allSubPorts) $ mOrElse (mtype allSubPorts) defaultNetType
258274
259275 public export
260276 typeOf : MultiConnection ms m subMs -> SVObject
261277 typeOf (MkMC (Just f) _ _ _ ) = typeOf (topSnks m) f
262278 typeOf (MkMC _ _ (Just f) _ ) = typeOf (topSrcs m) f
263- typeOf (MkMC _ ssk _ ssc) = mOrElse (mtype (subSnks ms m subMs) ssk) $ mOrElse (mtype (subSrcs ms m subMs) ssc) defaultNetType
279+ typeOf (MkMC _ ssk _ ssc) = resolveConnType {ms} {m} { subMs} ssk ssc
264280
265281 public export
266282 data MMC : (ms : ModuleSigsList) -> (m : ModuleSig) -> (subMs : FinsList ms.length) -> Type where
You can’t perform that action at this time.
0 commit comments