From 5e57da15cbf5d9fdb195991201967f76fda1b5b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Thu, 9 Oct 2025 18:52:24 +0300 Subject: [PATCH 1/3] WIP --- cuddle.cabal | 1 - src/Codec/CBOR/Cuddle/CDDL.hs | 2 +- src/Codec/CBOR/Cuddle/CDDL/CTree.hs | 154 ---------- src/Codec/CBOR/Cuddle/CDDL/Resolve.hs | 389 ++++++++++++++----------- src/Codec/CBOR/Cuddle/IndexMappable.hs | 21 -- 5 files changed, 212 insertions(+), 355 deletions(-) delete mode 100644 src/Codec/CBOR/Cuddle/CDDL/CTree.hs diff --git a/cuddle.cabal b/cuddle.cabal index 9ad5eb6..5b3f149 100644 --- a/cuddle.cabal +++ b/cuddle.cabal @@ -44,7 +44,6 @@ library Codec.CBOR.Cuddle.CBOR.Gen Codec.CBOR.Cuddle.CBOR.Validator Codec.CBOR.Cuddle.CDDL - Codec.CBOR.Cuddle.CDDL.CTree Codec.CBOR.Cuddle.CDDL.CtlOp Codec.CBOR.Cuddle.CDDL.Postlude Codec.CBOR.Cuddle.CDDL.Resolve diff --git a/src/Codec/CBOR/Cuddle/CDDL.hs b/src/Codec/CBOR/Cuddle/CDDL.hs index a06ab8a..d19e5c9 100644 --- a/src/Codec/CBOR/Cuddle/CDDL.hs +++ b/src/Codec/CBOR/Cuddle/CDDL.hs @@ -340,7 +340,7 @@ instance ForAllExtensions i CollectComments => CollectComments (TypeOrGroup i) field3: bytes, field4: ~time, ] - +Group (Note that leaving out the first unwrap operator in the latter example would lead to nesting the basic-header in its own array inside the advanced-header, while, with the unwrapped basic-header, the definition of the group inside diff --git a/src/Codec/CBOR/Cuddle/CDDL/CTree.hs b/src/Codec/CBOR/Cuddle/CDDL/CTree.hs deleted file mode 100644 index 4fda00d..0000000 --- a/src/Codec/CBOR/Cuddle/CDDL/CTree.hs +++ /dev/null @@ -1,154 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} - -module Codec.CBOR.Cuddle.CDDL.CTree where - -import Codec.CBOR.Cuddle.CDDL ( - Name, - OccurrenceIndicator, - RangeBound, - Value, - XCddl, - XTerm, - XXTopLevel, - XXType2, - ) -import Codec.CBOR.Cuddle.CDDL.CtlOp -import Codec.CBOR.Cuddle.Comments (Comment) -import Data.Hashable (Hashable) -import Data.List.NonEmpty qualified as NE -import Data.Map.Strict qualified as Map -import Data.Void (Void) -import Data.Word (Word64) -import GHC.Generics (Generic) - --------------------------------------------------------------------------------- - --- * Resolved CDDL Tree - --- --- This is a simplified representation of CDDL. It is technically more general - --- that is, the structure can represent invalid CDDL - but is in that way easier --- to manipulate. --------------------------------------------------------------------------------- - -type family CTreeExt i - -data CTreePhase - -newtype instance XTerm CTreePhase = CTreeXTerm Comment - deriving (Generic, Show, Eq, Ord, Hashable, Semigroup, Monoid) - -newtype instance XXTopLevel CTreePhase = CTreeXXTopLevel Comment - deriving (Generic, Show, Eq, Ord, Hashable) - -newtype instance XCddl CTreePhase = CTreeXCddl [Comment] - deriving (Generic, Show, Eq, Ord, Hashable) - -newtype instance XXType2 CTreePhase = CTreeXXType2 Void - deriving (Generic, Show, Eq, Ord, Hashable) - -data CTree i - = Literal Value - | Postlude PTerm - | Map [CTree i] - | Array [CTree i] - | Choice (NE.NonEmpty (CTree i)) - | Group [CTree i] - | KV {key :: CTree i, value :: CTree i, cut :: Bool} - | Occur {item :: CTree i, occurs :: OccurrenceIndicator} - | Range {from :: CTree i, to :: CTree i, inclusive :: RangeBound} - | Control {op :: CtlOp, target :: CTree i, controller :: CTree i} - | Enum (CTree i) - | Unwrap (CTree i) - | Tag Word64 (CTree i) - | CTreeE (CTreeExt i) - deriving (Generic) - -deriving instance Eq (Node f) => Eq (CTree f) - --- | Traverse the CTree, carrying out the given operation at each node -traverseCTree :: - Monad m => (CTreeExt i -> m (CTree j)) -> (CTree i -> m (CTree j)) -> CTree i -> m (CTree j) -traverseCTree _ _ (Literal a) = pure $ Literal a -traverseCTree _ _ (Postlude a) = pure $ Postlude a -traverseCTree _ atNode (Map xs) = Map <$> traverse atNode xs -traverseCTree _ atNode (Array xs) = Array <$> traverse atNode xs -traverseCTree _ atNode (Group xs) = Group <$> traverse atNode xs -traverseCTree _ atNode (Choice xs) = Choice <$> traverse atNode xs -traverseCTree _ atNode (KV k v c) = do - k' <- atNode k - v' <- atNode v - pure $ KV k' v' c -traverseCTree _ atNode (Occur i occ) = flip Occur occ <$> atNode i -traverseCTree _ atNode (Range f t inc) = do - f' <- atNode f - t' <- atNode t - pure $ Range f' t' inc -traverseCTree _ atNode (Control o t c) = do - t' <- atNode t - c' <- atNode c - pure $ Control o t' c' -traverseCTree _ atNode (Enum ref) = Enum <$> atNode ref -traverseCTree _ atNode (Unwrap ref) = Unwrap <$> atNode ref -traverseCTree _ atNode (Tag i ref) = Tag i <$> atNode ref -traverseCTree atExt _ (CTreeE x) = atExt x - -type Node i = CTreeExt i - -newtype CTreeRoot i = CTreeRoot (Map.Map (Name CTreePhase) (CTree i)) - deriving (Generic) - -deriving instance Show (CTree i) => Show (CTreeRoot i) - --- | --- --- CDDL predefines a number of names. This subsection summarizes these --- names, but please see Appendix D for the exact definitions. --- --- The following keywords for primitive datatypes are defined: --- --- "bool" Boolean value (major type 7, additional information 20 --- or 21). --- --- "uint" An unsigned integer (major type 0). --- --- "nint" A negative integer (major type 1). --- --- "int" An unsigned integer or a negative integer. --- --- "float16" A number representable as a half-precision float [IEEE754] --- (major type 7, additional information 25). --- --- "float32" A number representable as a single-precision float --- [IEEE754] (major type 7, additional information 26). --- --- --- "float64" A number representable as a double-precision float --- [IEEE754] (major type 7, additional information 27). --- --- "float" One of float16, float32, or float64. --- --- "bstr" or "bytes" A byte string (major type 2). --- --- "tstr" or "text" Text string (major type 3). --- --- (Note that there are no predefined names for arrays or maps; these --- are defined with the syntax given below.) -data PTerm - = PTBool - | PTUInt - | PTNInt - | PTInt - | PTHalf - | PTFloat - | PTDouble - | PTBytes - | PTText - | PTAny - | PTNil - | PTUndefined - deriving (Eq, Generic, Ord, Show) - -instance Hashable PTerm diff --git a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs index 6ca2392..ea873b5 100644 --- a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs +++ b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs @@ -33,7 +33,6 @@ module Codec.CBOR.Cuddle.CDDL.Resolve ( fullResolveCDDL, NameResolutionFailure (..), MonoReferenced, - MonoRef (..), ) where @@ -44,16 +43,31 @@ import Capability.Reader qualified as Reader (local) import Capability.Sink (HasSink) import Capability.Source (HasSource) import Capability.State (HasState, MonadState (..), modify) -import Codec.CBOR.Cuddle.CDDL as CDDL -import Codec.CBOR.Cuddle.CDDL.CTree ( - CTree (..), - CTreeExt, - CTreePhase, - CTreeRoot (..), - PTerm (..), - XXType2 (..), +import Codec.CBOR.Cuddle.CDDL ( + Assign (..), + CDDL, + GenericArg (..), + GenericParam (..), + Group (..), + GroupEntry (..), + GrpChoice (..), + MemberKey (..), + Name (..), + Rule (..), + TopLevel (..), + Type0 (..), + Type1 (..), + Type2 (..), + TypeOrGroup (..), + Value (..), + ValueVariant (..), + XCddl, + XTerm, + XXTopLevel, + XXType2, + cddlTopLevel, ) -import Codec.CBOR.Cuddle.CDDL.CTree qualified as CTree +import Codec.CBOR.Cuddle.CDDL.Postlude (PTerm (..)) import Control.Monad.Except (ExceptT (..), runExceptT) import Control.Monad.Reader (Reader, ReaderT (..), runReader) import Control.Monad.State.Strict (StateT (..)) @@ -63,56 +77,61 @@ import Data.Hashable #if __GLASGOW_HASKELL__ < 910 import Data.List (foldl') #endif +import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..)) +import Data.Bifunctor (Bifunctor (..)) import Data.List.NonEmpty qualified as NE import Data.Map.Strict qualified as Map import Data.Text qualified as T -import Data.Void (absurd) +import Data.Void (Void) +import Data.Word (Word64) import GHC.Generics (Generic) import Optics.Core -data ProvidedParameters a = ProvidedParameters - { parameters :: [Name CTreePhase] - , underlying :: a +data ProvidedParameters i = ProvidedParameters + { parameters :: [Name i] + , underlying :: TypeOrGroup i } - deriving (Generic, Functor, Show, Eq, Foldable, Traversable) + deriving (Generic) -instance Hashable a => Hashable (ProvidedParameters a) +instance Hashable (ProvidedParameters i) data Parametrised -type instance CTreeExt Parametrised = ProvidedParameters (CTree Parametrised) +newtype instance XXType2 Parametrised + = ParametrisedXXType2 (ProvidedParameters Parametrised) -------------------------------------------------------------------------------- -- 1. Rule extensions -------------------------------------------------------------------------------- -newtype PartialCTreeRoot i = PartialCTreeRoot (Map.Map (Name CTreePhase) (ProvidedParameters (CTree i))) +newtype PartialCTreeRoot i + = PartialCTreeRoot (Map.Map (Name i) (ProvidedParameters i)) deriving (Generic) -type CDDLMap = Map.Map (Name CTreePhase) (ProvidedParameters (TypeOrGroup CTreePhase)) +type CDDLMap i = Map.Map (Name i) (ProvidedParameters i) -toParametrised :: a -> Maybe (GenericParam CTreePhase) -> ProvidedParameters a +toParametrised :: TypeOrGroup i -> Maybe (GenericParam i) -> ProvidedParameters i toParametrised a Nothing = ProvidedParameters [] a toParametrised a (Just (GenericParam gps)) = ProvidedParameters (NE.toList gps) a -asMap :: CDDL CTreePhase -> CDDLMap +asMap :: CDDL i -> CDDLMap i asMap cddl = foldl' go Map.empty rules where rules = cddlTopLevel cddl go x (XXTopLevel _) = x go x (TopLevelRule r) = assignOrExtend x r - assignOrExtend :: CDDLMap -> Rule CTreePhase -> CDDLMap + assignOrExtend :: CDDLMap i -> Rule i -> CDDLMap i assignOrExtend m (Rule n gps assign tog _) = case assign of -- Equals assignment AssignEq -> Map.insert n (toParametrised tog gps) m AssignExt -> Map.alter (extend tog gps) n m extend :: - TypeOrGroup CTreePhase -> - Maybe (GenericParam CTreePhase) -> - Maybe (ProvidedParameters (TypeOrGroup CTreePhase)) -> - Maybe (ProvidedParameters (TypeOrGroup CTreePhase)) + TypeOrGroup i -> + Maybe (GenericParam i) -> + Maybe (ProvidedParameters i) -> + Maybe (ProvidedParameters i) extend tog _gps (Just existing) = case (underlying existing, tog) of (TOGType _, TOGType (Type0 new)) -> Just $ @@ -137,86 +156,77 @@ asMap cddl = foldl' go Map.empty rules data OrReferenced -type instance CTreeExt OrReferenced = OrRef +data instance XTerm OrReferenced = OrReferencedXTerm + deriving (Eq, Show) + +data instance XCddl OrReferenced = OrReferencedXCddl + deriving (Eq, Show) + +newtype instance XXTopLevel OrReferenced = OrReferencedXXTopLevel Void + deriving (Eq, Show) -- | Indicates that an item may be referenced rather than defined. -data OrRef +data instance XXType2 OrReferenced = -- | Reference to another node with possible generic arguments supplied - Ref (Name CTreePhase) [CTree OrReferenced] + Ref (Name OrReferenced) [TypeOrGroup OrReferenced] deriving (Eq, Show) type RefCTree = PartialCTreeRoot OrReferenced -deriving instance Show (CTree OrReferenced) - deriving instance Show (PartialCTreeRoot OrReferenced) -- | Build a CTree incorporating references. -- -- This translation cannot fail. -buildRefCTree :: CDDLMap -> RefCTree -buildRefCTree rules = PartialCTreeRoot $ toCTreeRule <$> rules +buildRefCTree :: CDDLMap i -> RefCTree +buildRefCTree rules = PartialCTreeRoot $ bimap mapIndex toCTreeRule rules where toCTreeRule :: - ProvidedParameters (TypeOrGroup CTreePhase) -> - ProvidedParameters (CTree OrReferenced) - toCTreeRule = fmap toCTreeTOG - - toCTreeTOG :: TypeOrGroup CTreePhase -> CTree OrReferenced - toCTreeTOG (TOGType t0) = toCTreeT0 t0 - toCTreeTOG (TOGGroup ge) = toCTreeGroupEntry ge - - toCTreeT0 :: Type0 CTreePhase -> CTree OrReferenced - toCTreeT0 (Type0 (t1 NE.:| [])) = toCTreeT1 t1 - toCTreeT0 (Type0 xs) = CTree.Choice $ toCTreeT1 <$> xs - - toCTreeT1 :: Type1 CTreePhase -> CTree OrReferenced - toCTreeT1 (Type1 t2 Nothing _) = toCTreeT2 t2 - toCTreeT1 (Type1 t2 (Just (op, t2')) _) = case op of - RangeOp bound -> - CTree.Range - { CTree.from = toCTreeT2 t2 - , CTree.to = toCTreeT2 t2' - , CTree.inclusive = bound - } - CtrlOp ctlop -> - CTree.Control - { CTree.op = ctlop - , CTree.target = toCTreeT2 t2 - , CTree.controller = toCTreeT2 t2' - } - - toCTreeT2 :: Type2 CTreePhase -> CTree OrReferenced - toCTreeT2 (T2Value v) = CTree.Literal v - toCTreeT2 (T2Name n garg) = CTreeE $ Ref n (fromGenArgs garg) + ProvidedParameters i -> + ProvidedParameters OrReferenced + toCTreeRule (ProvidedParameters ns t) = ProvidedParameters (undefined <$> ns) (toCTreeTOG t) + + toCTreeTOG :: TypeOrGroup i -> TypeOrGroup OrReferenced + toCTreeTOG (TOGType t0) = TOGType $ toCTreeT0 t0 + toCTreeTOG (TOGGroup ge) = TOGGroup $ toCTreeGroupEntry ge + + toCTreeT0 :: Type0 i -> Type0 OrReferenced + toCTreeT0 (Type0 ts) = Type0 $ toCTreeT1 <$> ts + + toCTreeT1 :: Type1 i -> Type1 OrReferenced + toCTreeT1 (Type1 t mr e) = Type1 (toCTreeT2 t) (second toCTreeT2 <$> mr) (mapIndex e) + + toCTreeT2 :: Type2 i -> Type2 OrReferenced + toCTreeT2 (T2Value v) = T2Value v + toCTreeT2 (T2Name n garg) = XXType2 $ Ref (mapIndex n) (fromGenArgs garg) toCTreeT2 (T2Group t0) = -- This behaviour seems questionable, but I don't really see how better to -- interpret the spec here. - toCTreeT0 t0 - toCTreeT2 (T2Map g) = toCTreeMap g - toCTreeT2 (T2Array g) = toCTreeArray g + T2Group $ toCTreeT0 t0 + toCTreeT2 (T2Map g) = T2Map $ toCTreeMap g + toCTreeT2 (T2Array g) = T2Array $ toCTreeArray g toCTreeT2 (T2Unwrapped n margs) = - CTree.Unwrap . CTreeE $ - Ref n (fromGenArgs margs) - toCTreeT2 (T2Enum g) = toCTreeEnum g - toCTreeT2 (T2EnumRef n margs) = CTreeE . Ref n $ fromGenArgs margs - toCTreeT2 (T2Tag Nothing t0) = + undefined + -- CTree.Unwrap . CTreeE $ + -- Ref n (fromGenArgs margs) + toCTreeT2 (T2Enum g) = T2Enum $ toCTreeEnum g + toCTreeT2 (T2EnumRef n margs) = XXType2 . Ref (mapIndex n) $ fromGenArgs margs + toCTreeT2 (T2Tag mtag t0) = -- Currently not validating tags - toCTreeT0 t0 - toCTreeT2 (T2Tag (Just tag) t0) = - CTree.Tag tag $ toCTreeT0 t0 + T2Tag mtag $ toCTreeT0 t0 toCTreeT2 (T2DataItem 7 (Just mmin)) = toCTreeDataItem mmin toCTreeT2 (T2DataItem _maj _mmin) = -- We don't validate numerical items yet - CTree.Postlude PTAny - toCTreeT2 T2Any = CTree.Postlude PTAny - toCTreeT2 (XXType2 (CTreeXXType2 v)) = absurd v + T2Any + toCTreeT2 T2Any = T2Any + toCTreeT2 (XXType2 x) = undefined + toCTreeDataItem :: Word64 -> Type2 OrReferenced toCTreeDataItem 20 = - CTree.Literal $ Value (VBool False) mempty + T2Value $ Value (VBool False) mempty toCTreeDataItem 21 = - CTree.Literal $ Value (VBool True) mempty + T2Value $ Value (VBool True) mempty toCTreeDataItem 25 = CTree.Postlude PTHalf toCTreeDataItem 26 = @@ -226,92 +236,105 @@ buildRefCTree rules = PartialCTreeRoot $ toCTreeRule <$> rules toCTreeDataItem 23 = CTree.Postlude PTUndefined toCTreeDataItem _ = - CTree.Postlude PTAny - - toCTreeGroupEntry :: GroupEntry CTreePhase -> CTree OrReferenced - toCTreeGroupEntry (GroupEntry (Just occi) (GEType mmkey t0) _) = - CTree.Occur - { CTree.item = toKVPair mmkey t0 - , CTree.occurs = occi - } - toCTreeGroupEntry (GroupEntry Nothing (GEType mmkey t0) _) = toKVPair mmkey t0 - toCTreeGroupEntry (GroupEntry (Just occi) (GERef n margs) _) = - CTree.Occur - { CTree.item = CTreeE $ Ref n (fromGenArgs margs) - , CTree.occurs = occi - } - toCTreeGroupEntry (GroupEntry Nothing (GERef n margs) _) = CTreeE $ Ref n (fromGenArgs margs) - toCTreeGroupEntry (GroupEntry (Just occi) (GEGroup g) _) = - CTree.Occur - { CTree.item = groupToGroup g - , CTree.occurs = occi - } - toCTreeGroupEntry (GroupEntry Nothing (GEGroup g) _) = groupToGroup g - - fromGenArgs :: Maybe (GenericArg CTreePhase) -> [CTree OrReferenced] - fromGenArgs = maybe [] (\(GenericArg xs) -> NE.toList $ fmap toCTreeT1 xs) + T2Any + + toCTreeGroupEntry :: GroupEntry i -> GroupEntry OrReferenced + toCTreeGroupEntry = undefined + -- toCTreeGroupEntry (GroupEntry (Just occi) (GEType mmkey t0) _) = + -- CTree.Occur + -- { CTree.item = toKVPair mmkey t0 + -- , CTree.occurs = occi + -- } + -- toCTreeGroupEntry (GroupEntry Nothing (GEType mmkey t0) _) = toKVPair mmkey t0 + -- toCTreeGroupEntry (GroupEntry (Just occi) (GERef n margs) _) = + -- CTree.Occur + -- { CTree.item = CTreeE $ Ref n (fromGenArgs margs) + -- , CTree.occurs = occi + -- } + -- toCTreeGroupEntry (GroupEntry Nothing (GERef n margs) _) = CTreeE $ Ref n (fromGenArgs margs) + -- toCTreeGroupEntry (GroupEntry (Just occi) (GEGroup g) _) = + -- CTree.Occur + -- { CTree.item = groupToGroup g + -- , CTree.occurs = occi + -- } + -- toCTreeGroupEntry (GroupEntry Nothing (GEGroup g) _) = groupToGroup g + + fromGenArgs :: Maybe (GenericArg i) -> [TypeOrGroup OrReferenced] + fromGenArgs = maybe [] (\(GenericArg xs) -> NE.toList $ fmap (undefined . toCTreeT1) xs) -- Interpret a group as an enumeration. Note that we float out the -- choice options - toCTreeEnum :: Group CTreePhase -> CTree OrReferenced - toCTreeEnum (CDDL.Group (a NE.:| [])) = - CTree.Enum . CTree.Group $ toCTreeGroupEntry <$> gcGroupEntries a - toCTreeEnum (CDDL.Group xs) = - CTree.Choice $ CTree.Enum . CTree.Group . fmap toCTreeGroupEntry <$> groupEntries + toCTreeEnum :: Group i -> Group OrReferenced + toCTreeEnum (Group (a NE.:| [])) = + undefined -- CTree.Enum . CTree.Group $ toCTreeGroupEntry <$> gcGroupEntries a + toCTreeEnum (Group xs) = + undefined -- CTree.Choice $ CTree.Enum . CTree.Group . fmap toCTreeGroupEntry <$> groupEntries where groupEntries = fmap gcGroupEntries xs -- Embed a group in another group, again floating out the choice options - groupToGroup :: Group CTreePhase -> CTree OrReferenced - groupToGroup (CDDL.Group (a NE.:| [])) = - CTree.Group $ fmap toCTreeGroupEntry (gcGroupEntries a) - groupToGroup (CDDL.Group xs) = - CTree.Choice $ fmap (CTree.Group . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) - - toKVPair :: Maybe (MemberKey CTreePhase) -> Type0 CTreePhase -> CTree OrReferenced - toKVPair Nothing t0 = toCTreeT0 t0 - toKVPair (Just mkey) t0 = - CTree.KV - { CTree.key = toCTreeMemberKey mkey - , CTree.value = toCTreeT0 t0 - , -- TODO Handle cut semantics - CTree.cut = False - } + groupToGroup :: Group i -> Group OrReferenced + groupToGroup (Group (a NE.:| [])) = + undefined -- Group $ fmap toCTreeGroupEntry (gcGroupEntries a) + groupToGroup (Group xs) = + undefined -- CTree.Choice $ fmap (Group . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) + toKVPair :: Maybe (MemberKey i) -> Type0 i -> TypeOrGroup OrReferenced + toKVPair = undefined + -- toKVPair Nothing t0 = toCTreeT0 t0 + -- toKVPair (Just mkey) t0 = + -- CTree.KV + -- { CTree.key = toCTreeMemberKey mkey + -- , CTree.value = toCTreeT0 t0 + -- , -- TODO Handle cut semantics + -- CTree.cut = False + -- } -- Interpret a group as a map. Note that we float out the choice options - toCTreeMap :: Group CTreePhase -> CTree OrReferenced - toCTreeMap (CDDL.Group (a NE.:| [])) = CTree.Map $ fmap toCTreeGroupEntry (gcGroupEntries a) - toCTreeMap (CDDL.Group xs) = - CTree.Choice $ - fmap (CTree.Map . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) + toCTreeMap :: Group i -> Type0 OrReferenced + -- toCTreeMap (Group (a NE.:| [])) = CTree.Map $ fmap toCTreeGroupEntry (gcGroupEntries a) + toCTreeMap (Group xs) = + Type0 $ + xs <&> \(GrpChoice ges c) -> + Type1 + (T2Map . Group . NE.singleton $ GrpChoice (toCTreeGroupEntry <$> ges) (mapIndex c)) + Nothing + mempty + -- fmap (CTree.Map . fmap toCTreeGroupEntry . gcGroupEntries) xs -- Interpret a group as an array. Note that we float out the choice -- options - toCTreeArray :: Group CTreePhase -> CTree OrReferenced - toCTreeArray (CDDL.Group (a NE.:| [])) = - CTree.Array $ fmap toCTreeGroupEntry (gcGroupEntries a) - toCTreeArray (CDDL.Group xs) = - CTree.Choice $ - fmap (CTree.Array . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) - - toCTreeMemberKey :: MemberKey CTreePhase -> CTree OrReferenced - toCTreeMemberKey (MKValue v) = CTree.Literal v - toCTreeMemberKey (MKBareword (Name n _)) = CTree.Literal (Value (VText n) mempty) - toCTreeMemberKey (MKType t1) = toCTreeT1 t1 + toCTreeArray :: Group i -> Type0 OrReferenced + toCTreeArray (Group xs) = + Type0 $ + xs <&> \(GrpChoice ges c) -> + Type1 + (T2Array . Group . NE.singleton $ GrpChoice (toCTreeGroupEntry <$> ges) (mapIndex c)) + Nothing + mempty + -- toCTreeArray (Group (a NE.:| [])) = + -- CTree.Array $ fmap toCTreeGroupEntry (gcGroupEntries a) + -- toCTreeArray (Group xs) = + -- CTree.Choice $ + -- fmap (CTree.Array . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) + + toCTreeMemberKey :: MemberKey i -> Type2 OrReferenced + toCTreeMemberKey (MKValue v) = T2Value v + toCTreeMemberKey (MKBareword (Name n _)) = T2Value (Value (VText n) mempty) + toCTreeMemberKey (MKType t1) = undefined . MKType $ toCTreeT1 t1 -------------------------------------------------------------------------------- -- 3. Name resolution -------------------------------------------------------------------------------- data NameResolutionFailure - = UnboundReference (Name CTreePhase) - | MismatchingArgs (Name CTreePhase) [Name CTreePhase] - | ArgsToPostlude PTerm [CTree OrReferenced] + = UnboundReference (Name OrReferenced) + | MismatchingArgs (Name OrReferenced) [Name OrReferenced] + | ArgsToPostlude PTerm [TypeOrGroup OrReferenced] deriving (Show) -deriving instance Eq (CTree.Node OrReferenced) => Eq NameResolutionFailure +deriving instance Eq NameResolutionFailure -postludeBinding :: Map.Map (Name CTreePhase) PTerm +postludeBinding :: Map.Map (Name phase) PTerm postludeBinding = Map.fromList [ (Name "bool" mempty, PTBool) @@ -331,29 +354,32 @@ postludeBinding = ] data BindingEnv i j = BindingEnv - { global :: Map.Map (Name CTreePhase) (ProvidedParameters (CTree i)) + { global :: Map.Map (Name i) (ProvidedParameters i) -- ^ Global name bindings via 'RuleDef' - , local :: Map.Map (Name CTreePhase) (CTree j) + , local :: Map.Map (Name j) (TypeOrGroup j) -- ^ Local bindings for generic parameters } deriving (Generic) data DistReferenced -type instance CTreeExt DistReferenced = DistRef +data instance XTerm DistReferenced = DistReferencedXTerm + deriving (Eq, Show) + +data instance XCddl DistReferenced = DistReferencedXCddl + deriving (Eq, Show) + +data instance XXTopLevel DistReferenced = DistReferencedXXTopLevel + deriving (Eq, Show) -data DistRef +data instance XXType2 DistReferenced = -- | Reference to a generic parameter - GenericRef (Name CTreePhase) + GenericRef (Name DistReferenced) | -- | Reference to a rule definition, possibly with generic arguments - RuleRef (Name CTreePhase) [CTree DistReferenced] + RuleRef (Name DistReferenced) [TypeOrGroup DistReferenced] deriving (Eq, Generic, Show) -instance Hashable DistRef - -deriving instance Show (CTree DistReferenced) - -instance Hashable (CTree DistReferenced) +instance Hashable (TypeOrGroup DistReferenced) deriving instance Show (PartialCTreeRoot DistReferenced) @@ -363,8 +389,8 @@ instance Hashable (PartialCTreeRoot DistReferenced) resolveRef :: BindingEnv OrReferenced OrReferenced -> - CTree.Node OrReferenced -> - Either NameResolutionFailure (CTree DistReferenced) + XXType2 OrReferenced -> + Either NameResolutionFailure (TypeOrGroup DistReferenced) resolveRef env (Ref n args) = case Map.lookup n postludeBinding of Just pterm -> case args of [] -> Right $ CTree.Postlude pterm @@ -375,7 +401,11 @@ resolveRef env (Ref n args) = case Map.lookup n postludeBinding of then let localBinds = Map.fromList $ zip params' args newEnv = env & #local %~ Map.union localBinds - in CTreeE . RuleRef n <$> traverse (resolveCTree newEnv) args + in Right . TOGType . Type0 . NE.singleton $ + Type1 + (XXType2 . RuleRef (mapIndex n) <$> traverse (resolveCTree newEnv) args) + undefined + undefined else Left $ MismatchingArgs n params' Nothing -> case Map.lookup n (local env) of Just _ -> Right . CTreeE $ GenericRef n @@ -383,8 +413,8 @@ resolveRef env (Ref n args) = case Map.lookup n postludeBinding of resolveCTree :: BindingEnv OrReferenced OrReferenced -> - CTree OrReferenced -> - Either NameResolutionFailure (CTree DistReferenced) + TypeOrGroup OrReferenced -> + Either NameResolutionFailure (TypeOrGroup DistReferenced) resolveCTree e = CTree.traverseCTree (resolveRef e) (resolveCTree e) buildResolvedCTree :: @@ -404,20 +434,20 @@ buildResolvedCTree (PartialCTreeRoot ct) = PartialCTreeRoot <$> traverse go ct data MonoReferenced -type instance CTreeExt MonoReferenced = MonoRef (CTree MonoReferenced) +data instance XTerm MonoReferenced = MonoReferencedXTerm + deriving (Show) -newtype MonoRef a - = MRuleRef (Name CTreePhase) - deriving (Functor, Show) +newtype instance XXType2 MonoReferenced = MRuleRef (Name MonoReferenced) + deriving (Show) -deriving instance Show (CTree MonoReferenced) +deriving instance Show (TypeOrGroup MonoReferenced) deriving instance Show (PartialCTreeRoot MonoReferenced) type MonoEnv = BindingEnv DistReferenced MonoReferenced -- | We introduce additional bindings in the state -type MonoState = Map.Map (Name CTreePhase) (CTree MonoReferenced) +type MonoState = Map.Map (Name MonoReferenced) (TypeOrGroup MonoReferenced) -- | Monad to run the monomorphisation process. We need some additional -- capabilities for this, so 'Either' doesn't fully cut it anymore. @@ -439,10 +469,10 @@ newtype MonoM a = MonoM deriving ( HasSource "local" - (Map.Map (Name CTreePhase) (CTree MonoReferenced)) + (Map.Map (Name MonoReferenced) (TypeOrGroup MonoReferenced)) , HasReader "local" - (Map.Map (Name CTreePhase) (CTree MonoReferenced)) + (Map.Map (Name MonoReferenced) (TypeOrGroup MonoReferenced)) ) via Field "local" @@ -456,10 +486,10 @@ newtype MonoM a = MonoM deriving ( HasSource "global" - (Map.Map (Name CTreePhase) (ProvidedParameters (CTree DistReferenced))) + (Map.Map (Name DistReferenced) (ProvidedParameters DistReferenced)) , HasReader "global" - (Map.Map (Name CTreePhase) (ProvidedParameters (CTree DistReferenced))) + (Map.Map (Name DistReferenced) (ProvidedParameters DistReferenced)) ) via Field "global" @@ -485,7 +515,7 @@ throwNR :: NameResolutionFailure -> MonoM a throwNR = throw @"nameResolution" -- | Synthesize a monomorphic rule definition, returning the name -synthMono :: Name CTreePhase -> [CTree DistReferenced] -> MonoM (Name CTreePhase) +synthMono :: Name DistReferenced -> [TypeOrGroup DistReferenced] -> MonoM (Name phase) synthMono n@(Name origName _) args = let fresh = -- % is not a valid CBOR name, so this should avoid conflict @@ -494,7 +524,7 @@ synthMono n@(Name origName _) args = -- Lookup the original name in the global bindings globalBinds <- ask @"global" case Map.lookup n globalBinds of - Just (ProvidedParameters [] _) -> throwNR $ MismatchingArgs n [] + Just (ProvidedParameters [] _) -> throwNR $ MismatchingArgs (mapIndex n) [] Just (ProvidedParameters params' r) -> if length params' == length args then do @@ -508,8 +538,8 @@ synthMono n@(Name origName _) args = pure fresh resolveGenericRef :: - CTree.Node DistReferenced -> - MonoM (CTree MonoReferenced) + XXType2 DistReferenced -> + MonoM (TypeOrGroup MonoReferenced) resolveGenericRef (RuleRef n []) = pure . CTreeE $ MRuleRef n resolveGenericRef (RuleRef n args) = do fresh <- synthMono n args @@ -521,10 +551,12 @@ resolveGenericRef (GenericRef n) = do Nothing -> throwNR $ UnboundReference n resolveGenericCTree :: - CTree DistReferenced -> - MonoM (CTree MonoReferenced) + TypeOrGroup DistReferenced -> + MonoM (TypeOrGroup MonoReferenced) resolveGenericCTree = CTree.traverseCTree resolveGenericRef resolveGenericCTree +data CTreeRoot i = CTreeRoot + -- | Monomorphise the CTree -- -- Concretely, for each reference in the tree to a generic rule, we synthesize a @@ -552,7 +584,8 @@ buildMonoCTree (PartialCTreeRoot ct) = do -- Combined resolution -------------------------------------------------------------------------------- -fullResolveCDDL :: CDDL CTreePhase -> Either NameResolutionFailure (CTreeRoot MonoReferenced) +fullResolveCDDL :: + CDDL phase -> Either NameResolutionFailure (CTreeRoot MonoReferenced) fullResolveCDDL cddl = do let refCTree = buildRefCTree (asMap cddl) rCTree <- buildResolvedCTree refCTree diff --git a/src/Codec/CBOR/Cuddle/IndexMappable.hs b/src/Codec/CBOR/Cuddle/IndexMappable.hs index eba4d78..a174a7e 100644 --- a/src/Codec/CBOR/Cuddle/IndexMappable.hs +++ b/src/Codec/CBOR/Cuddle/IndexMappable.hs @@ -23,13 +23,6 @@ import Codec.CBOR.Cuddle.CDDL ( XXTopLevel, XXType2, ) -import Codec.CBOR.Cuddle.CDDL.CTree ( - CTreePhase, - XCddl (..), - XTerm (..), - XXTopLevel (..), - XXType2 (..), - ) import Codec.CBOR.Cuddle.Huddle (HuddleStage, XCddl (..), XTerm (..), XXTopLevel (..), XXType2 (..)) import Codec.CBOR.Cuddle.Parser (ParserStage, XCddl (..), XTerm (..), XXTopLevel (..), XXType2 (..)) import Codec.CBOR.Cuddle.Pretty (PrettyStage, XCddl (..), XTerm (..), XXTopLevel (..)) @@ -186,20 +179,6 @@ instance IndexMappable XXType2 ParserStage PrettyStage where instance IndexMappable XXTopLevel ParserStage PrettyStage where mapIndex (ParserXXTopLevel c) = PrettyXXTopLevel c --- ParserStage -> CTreePhase - -instance IndexMappable XCddl ParserStage CTreePhase where - mapIndex (ParserXCddl c) = CTreeXCddl c - -instance IndexMappable XXTopLevel ParserStage CTreePhase where - mapIndex (ParserXXTopLevel c) = CTreeXXTopLevel c - -instance IndexMappable XXType2 ParserStage CTreePhase where - mapIndex (ParserXXType2 c) = CTreeXXType2 c - -instance IndexMappable XTerm ParserStage CTreePhase where - mapIndex (ParserXTerm c) = CTreeXTerm c - -- ParserStage -> HuddleStage instance IndexMappable XCddl ParserStage HuddleStage where From 409412046eb01a07116e51912b19fd3ed207edf0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Mon, 13 Oct 2025 12:48:43 +0300 Subject: [PATCH 2/3] WIP --- src/Codec/CBOR/Cuddle/CDDL/Resolve.hs | 177 ++++++++++++-------------- 1 file changed, 83 insertions(+), 94 deletions(-) diff --git a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs index ea873b5..fe4e294 100644 --- a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs +++ b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs @@ -68,17 +68,16 @@ import Codec.CBOR.Cuddle.CDDL ( cddlTopLevel, ) import Codec.CBOR.Cuddle.CDDL.Postlude (PTerm (..)) +import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..)) import Control.Monad.Except (ExceptT (..), runExceptT) import Control.Monad.Reader (Reader, ReaderT (..), runReader) import Control.Monad.State.Strict (StateT (..)) +import Data.Bifunctor (Bifunctor (..)) +import Data.Foldable (Foldable (..)) import Data.Generics.Product import Data.Generics.Sum import Data.Hashable -#if __GLASGOW_HASKELL__ < 910 -import Data.List (foldl') -#endif -import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..)) -import Data.Bifunctor (Bifunctor (..)) +import Data.List.NonEmpty (NonEmpty (..)) import Data.List.NonEmpty qualified as NE import Data.Map.Strict qualified as Map import Data.Text qualified as T @@ -168,7 +167,9 @@ newtype instance XXTopLevel OrReferenced = OrReferencedXXTopLevel Void -- | Indicates that an item may be referenced rather than defined. data instance XXType2 OrReferenced = -- | Reference to another node with possible generic arguments supplied - Ref (Name OrReferenced) [TypeOrGroup OrReferenced] + -- The boolean field determines whether the reference should be unwrapped + Ref Bool (Name OrReferenced) [Type1 OrReferenced] + | OrPostlude PTerm deriving (Eq, Show) type RefCTree = PartialCTreeRoot OrReferenced @@ -184,42 +185,45 @@ buildRefCTree rules = PartialCTreeRoot $ bimap mapIndex toCTreeRule rules toCTreeRule :: ProvidedParameters i -> ProvidedParameters OrReferenced - toCTreeRule (ProvidedParameters ns t) = ProvidedParameters (undefined <$> ns) (toCTreeTOG t) + toCTreeRule (ProvidedParameters ns t) = ProvidedParameters (mapIndex <$> ns) (toCTreeTOG t) toCTreeTOG :: TypeOrGroup i -> TypeOrGroup OrReferenced toCTreeTOG (TOGType t0) = TOGType $ toCTreeT0 t0 toCTreeTOG (TOGGroup ge) = TOGGroup $ toCTreeGroupEntry ge toCTreeT0 :: Type0 i -> Type0 OrReferenced - toCTreeT0 (Type0 ts) = Type0 $ toCTreeT1 <$> ts - - toCTreeT1 :: Type1 i -> Type1 OrReferenced - toCTreeT1 (Type1 t mr e) = Type1 (toCTreeT2 t) (second toCTreeT2 <$> mr) (mapIndex e) + toCTreeT0 (Type0 xs) = foldMap (Type0 . toCTreeT1) xs - toCTreeT2 :: Type2 i -> Type2 OrReferenced - toCTreeT2 (T2Value v) = T2Value v - toCTreeT2 (T2Name n garg) = XXType2 $ Ref (mapIndex n) (fromGenArgs garg) + toCTreeT1 :: Type1 i -> NonEmpty (Type1 OrReferenced) + toCTreeT1 (Type1 t mr _) = (\x y -> Type1 x y mempty) <$> t' <*> r' + where + t' = toCTreeT2 t + r' = case mr of + Just (op, x) -> Just . (op,) <$> toCTreeT2 x + Nothing -> NE.singleton Nothing + + toCTreeT2 :: Type2 i -> NonEmpty (Type2 OrReferenced) + toCTreeT2 (T2Value v) = NE.singleton $ T2Value v + toCTreeT2 (T2Name n garg) = NE.singleton . XXType2 $ Ref False (mapIndex n) (fromGenArgs garg) toCTreeT2 (T2Group t0) = -- This behaviour seems questionable, but I don't really see how better to -- interpret the spec here. - T2Group $ toCTreeT0 t0 - toCTreeT2 (T2Map g) = T2Map $ toCTreeMap g - toCTreeT2 (T2Array g) = T2Array $ toCTreeArray g + NE.singleton . T2Group $ toCTreeT0 t0 + toCTreeT2 (T2Map g) = liftChoice T2Map g + toCTreeT2 (T2Array g) = liftChoice T2Map g toCTreeT2 (T2Unwrapped n margs) = - undefined - -- CTree.Unwrap . CTreeE $ - -- Ref n (fromGenArgs margs) - toCTreeT2 (T2Enum g) = T2Enum $ toCTreeEnum g - toCTreeT2 (T2EnumRef n margs) = XXType2 . Ref (mapIndex n) $ fromGenArgs margs + NE.singleton . XXType2 $ Ref True (mapIndex n) (fromGenArgs margs) + toCTreeT2 (T2Enum g) = NE.singleton . T2Enum $ toCTreeEnum g + toCTreeT2 (T2EnumRef n margs) = NE.singleton . XXType2 . Ref False (mapIndex n) $ fromGenArgs margs toCTreeT2 (T2Tag mtag t0) = -- Currently not validating tags - T2Tag mtag $ toCTreeT0 t0 + NE.singleton . T2Tag mtag $ toCTreeT0 t0 toCTreeT2 (T2DataItem 7 (Just mmin)) = - toCTreeDataItem mmin + NE.singleton $ toCTreeDataItem mmin toCTreeT2 (T2DataItem _maj _mmin) = -- We don't validate numerical items yet - T2Any - toCTreeT2 T2Any = T2Any + NE.singleton T2Any + toCTreeT2 T2Any = NE.singleton T2Any toCTreeT2 (XXType2 x) = undefined toCTreeDataItem :: Word64 -> Type2 OrReferenced @@ -228,13 +232,13 @@ buildRefCTree rules = PartialCTreeRoot $ bimap mapIndex toCTreeRule rules toCTreeDataItem 21 = T2Value $ Value (VBool True) mempty toCTreeDataItem 25 = - CTree.Postlude PTHalf + XXType2 $ OrPostlude PTHalf toCTreeDataItem 26 = - CTree.Postlude PTFloat + XXType2 $ OrPostlude PTFloat toCTreeDataItem 27 = - CTree.Postlude PTDouble + XXType2 $ OrPostlude PTDouble toCTreeDataItem 23 = - CTree.Postlude PTUndefined + XXType2 $ OrPostlude PTUndefined toCTreeDataItem _ = T2Any @@ -259,25 +263,24 @@ buildRefCTree rules = PartialCTreeRoot $ bimap mapIndex toCTreeRule rules -- } -- toCTreeGroupEntry (GroupEntry Nothing (GEGroup g) _) = groupToGroup g - fromGenArgs :: Maybe (GenericArg i) -> [TypeOrGroup OrReferenced] - fromGenArgs = maybe [] (\(GenericArg xs) -> NE.toList $ fmap (undefined . toCTreeT1) xs) + fromGenArgs :: Maybe (GenericArg i) -> [Type1 OrReferenced] + fromGenArgs = maybe [] (\(GenericArg xs) -> NE.toList $ foldMap toCTreeT1 xs) -- Interpret a group as an enumeration. Note that we float out the -- choice options toCTreeEnum :: Group i -> Group OrReferenced - toCTreeEnum (Group (a NE.:| [])) = - undefined -- CTree.Enum . CTree.Group $ toCTreeGroupEntry <$> gcGroupEntries a - toCTreeEnum (Group xs) = - undefined -- CTree.Choice $ CTree.Enum . CTree.Group . fmap toCTreeGroupEntry <$> groupEntries - where - groupEntries = fmap gcGroupEntries xs + toCTreeEnum g = undefined $ liftChoice T2Enum g + -- CTree.Enum . CTree.Group $ toCTreeGroupEntry <$> gcGroupEntries a + -- CTree.Choice $ CTree.Enum . CTree.Group . fmap toCTreeGroupEntry <$> groupEntries + -- where + -- groupEntries = fmap gcGroupEntries xs -- Embed a group in another group, again floating out the choice options groupToGroup :: Group i -> Group OrReferenced - groupToGroup (Group (a NE.:| [])) = - undefined -- Group $ fmap toCTreeGroupEntry (gcGroupEntries a) - groupToGroup (Group xs) = - undefined -- CTree.Choice $ fmap (Group . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) + groupToGroup g = + Group . fmap (\x -> GrpChoice [GroupEntry Nothing undefined mempty] mempty) $ + liftChoice undefined g + toKVPair :: Maybe (MemberKey i) -> Type0 i -> TypeOrGroup OrReferenced toKVPair = undefined -- toKVPair Nothing t0 = toCTreeT0 t0 @@ -290,37 +293,15 @@ buildRefCTree rules = PartialCTreeRoot $ bimap mapIndex toCTreeRule rules -- } -- Interpret a group as a map. Note that we float out the choice options - toCTreeMap :: Group i -> Type0 OrReferenced - -- toCTreeMap (Group (a NE.:| [])) = CTree.Map $ fmap toCTreeGroupEntry (gcGroupEntries a) - toCTreeMap (Group xs) = - Type0 $ - xs <&> \(GrpChoice ges c) -> - Type1 - (T2Map . Group . NE.singleton $ GrpChoice (toCTreeGroupEntry <$> ges) (mapIndex c)) - Nothing - mempty - -- fmap (CTree.Map . fmap toCTreeGroupEntry . gcGroupEntries) xs - - -- Interpret a group as an array. Note that we float out the choice - -- options - toCTreeArray :: Group i -> Type0 OrReferenced - toCTreeArray (Group xs) = - Type0 $ - xs <&> \(GrpChoice ges c) -> - Type1 - (T2Array . Group . NE.singleton $ GrpChoice (toCTreeGroupEntry <$> ges) (mapIndex c)) - Nothing - mempty - -- toCTreeArray (Group (a NE.:| [])) = - -- CTree.Array $ fmap toCTreeGroupEntry (gcGroupEntries a) - -- toCTreeArray (Group xs) = - -- CTree.Choice $ - -- fmap (CTree.Array . fmap toCTreeGroupEntry) (gcGroupEntries <$> xs) - - toCTreeMemberKey :: MemberKey i -> Type2 OrReferenced - toCTreeMemberKey (MKValue v) = T2Value v - toCTreeMemberKey (MKBareword (Name n _)) = T2Value (Value (VText n) mempty) - toCTreeMemberKey (MKType t1) = undefined . MKType $ toCTreeT1 t1 + liftChoice :: (Group OrReferenced -> Type2 OrReferenced) -> Group i -> NonEmpty (Type2 OrReferenced) + liftChoice f (Group xs) = + xs <&> \(GrpChoice ges c) -> + f . Group . NE.singleton $ GrpChoice (toCTreeGroupEntry <$> ges) (mapIndex c) + + toCTreeMemberKey :: MemberKey i -> MemberKey OrReferenced + toCTreeMemberKey (MKValue v) = MKValue v + toCTreeMemberKey (MKBareword n) = MKBareword $ mapIndex n + toCTreeMemberKey (MKType t1) = undefined $ MKType <$> toCTreeT1 t1 -------------------------------------------------------------------------------- -- 3. Name resolution @@ -356,7 +337,7 @@ postludeBinding = data BindingEnv i j = BindingEnv { global :: Map.Map (Name i) (ProvidedParameters i) -- ^ Global name bindings via 'RuleDef' - , local :: Map.Map (Name j) (TypeOrGroup j) + , local :: Map.Map (Name j) (Type1 j) -- ^ Local bindings for generic parameters } deriving (Generic) @@ -377,6 +358,7 @@ data instance XXType2 DistReferenced GenericRef (Name DistReferenced) | -- | Reference to a rule definition, possibly with generic arguments RuleRef (Name DistReferenced) [TypeOrGroup DistReferenced] + | DistPostlude PTerm deriving (Eq, Generic, Show) instance Hashable (TypeOrGroup DistReferenced) @@ -391,29 +373,36 @@ resolveRef :: BindingEnv OrReferenced OrReferenced -> XXType2 OrReferenced -> Either NameResolutionFailure (TypeOrGroup DistReferenced) -resolveRef env (Ref n args) = case Map.lookup n postludeBinding of - Just pterm -> case args of - [] -> Right $ CTree.Postlude pterm - xs -> Left $ ArgsToPostlude pterm xs - Nothing -> case Map.lookup n (global env) of - Just (parameters -> params') -> - if length params' == length args - then - let localBinds = Map.fromList $ zip params' args - newEnv = env & #local %~ Map.union localBinds - in Right . TOGType . Type0 . NE.singleton $ - Type1 - (XXType2 . RuleRef (mapIndex n) <$> traverse (resolveCTree newEnv) args) - undefined - undefined - else Left $ MismatchingArgs n params' - Nothing -> case Map.lookup n (local env) of - Just _ -> Right . CTreeE $ GenericRef n - Nothing -> Left $ UnboundReference n +resolveRef env = \case + Ref unwrap n args -> resolveRef_ unwrap n args + OrPostlude t -> undefined t + where + resolveRef_ :: + Bool -> + Name OrReferenced -> + [Type1 OrReferenced] -> + Either NameResolutionFailure (TypeOrGroup DistReferenced) + resolveRef_ unwrap n args = case Map.lookup n postludeBinding of + Just pterm -> case args of + [] -> Right . undefined . XXType2 $ DistPostlude pterm + xs -> Left $ ArgsToPostlude pterm $ undefined xs + Nothing -> case Map.lookup n (global env) of + Just (parameters -> params') -> + if length params' == length args + then do + let localBinds = Map.fromList $ zip params' args + newEnv = env & #local %~ Map.union localBinds + ref <- XXType2 . RuleRef (mapIndex n) <$> traverse (resolveCTree newEnv) args + Right . TOGType . Type0 . NE.singleton $ + Type1 ref Nothing mempty + else Left $ MismatchingArgs n params' + Nothing -> case Map.lookup n (local env) of + Just _ -> Right . undefined . XXType2 $ GenericRef (mapIndex n) + Nothing -> Left $ UnboundReference n resolveCTree :: BindingEnv OrReferenced OrReferenced -> - TypeOrGroup OrReferenced -> + Type1 OrReferenced -> Either NameResolutionFailure (TypeOrGroup DistReferenced) resolveCTree e = CTree.traverseCTree (resolveRef e) (resolveCTree e) From c965432d6737febe798bc80bd6e67c694c908f84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Mon, 13 Oct 2025 18:39:11 +0300 Subject: [PATCH 3/3] WIP --- src/Codec/CBOR/Cuddle/CDDL/Resolve.hs | 85 ++++++++++++++++++++++----- src/Codec/CBOR/Cuddle/Pretty.hs | 2 +- 2 files changed, 70 insertions(+), 17 deletions(-) diff --git a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs index fe4e294..fd2963a 100644 --- a/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs +++ b/src/Codec/CBOR/Cuddle/CDDL/Resolve.hs @@ -67,7 +67,6 @@ import Codec.CBOR.Cuddle.CDDL ( XXType2, cddlTopLevel, ) -import Codec.CBOR.Cuddle.CDDL.Postlude (PTerm (..)) import Codec.CBOR.Cuddle.IndexMappable (IndexMappable (..)) import Control.Monad.Except (ExceptT (..), runExceptT) import Control.Monad.Reader (Reader, ReaderT (..), runReader) @@ -224,7 +223,7 @@ buildRefCTree rules = PartialCTreeRoot $ bimap mapIndex toCTreeRule rules -- We don't validate numerical items yet NE.singleton T2Any toCTreeT2 T2Any = NE.singleton T2Any - toCTreeT2 (XXType2 x) = undefined + toCTreeT2 x@(XXType2 _) = NE.singleton $ mapIndex x toCTreeDataItem :: Word64 -> Type2 OrReferenced toCTreeDataItem 20 = @@ -404,18 +403,20 @@ resolveCTree :: BindingEnv OrReferenced OrReferenced -> Type1 OrReferenced -> Either NameResolutionFailure (TypeOrGroup DistReferenced) -resolveCTree e = CTree.traverseCTree (resolveRef e) (resolveCTree e) +resolveCTree e = undefined -- CTree.traverseCTree (resolveRef e) (resolveCTree e) buildResolvedCTree :: PartialCTreeRoot OrReferenced -> Either NameResolutionFailure (PartialCTreeRoot DistReferenced) -buildResolvedCTree (PartialCTreeRoot ct) = PartialCTreeRoot <$> traverse go ct +buildResolvedCTree (PartialCTreeRoot ct) = undefined -- PartialCTreeRoot <$> traverse go ct where go pn = - let args = parameters pn - localBinds = Map.fromList $ zip args (CTreeE . flip Ref [] <$> args) + let argNames = parameters pn + argTerms = (\x -> Type1 x Nothing mempty) . XXType2 . (\n -> Ref False n []) <$> argNames + localBinds = + Map.fromList $ zip argNames argTerms env = BindingEnv @OrReferenced @OrReferenced ct localBinds - in traverse (resolveCTree env) pn + in undefined pn -- traverse (resolveCTree env) pn -------------------------------------------------------------------------------- -- 4. Monomorphisation @@ -458,10 +459,10 @@ newtype MonoM a = MonoM deriving ( HasSource "local" - (Map.Map (Name MonoReferenced) (TypeOrGroup MonoReferenced)) + (Map.Map (Name MonoReferenced) (Type1 MonoReferenced)) , HasReader "local" - (Map.Map (Name MonoReferenced) (TypeOrGroup MonoReferenced)) + (Map.Map (Name MonoReferenced) (Type1 MonoReferenced)) ) via Field "local" @@ -504,7 +505,7 @@ throwNR :: NameResolutionFailure -> MonoM a throwNR = throw @"nameResolution" -- | Synthesize a monomorphic rule definition, returning the name -synthMono :: Name DistReferenced -> [TypeOrGroup DistReferenced] -> MonoM (Name phase) +synthMono :: Name DistReferenced -> [TypeOrGroup DistReferenced] -> MonoM (Name MonoReferenced) synthMono n@(Name origName _) args = let fresh = -- % is not a valid CBOR name, so this should avoid conflict @@ -517,32 +518,33 @@ synthMono n@(Name origName _) args = Just (ProvidedParameters params' r) -> if length params' == length args then do - rargs <- traverse resolveGenericCTree args + rargs <- undefined -- traverse resolveGenericCTree args let localBinds = Map.fromList $ zip params' rargs Reader.local @"local" (Map.union localBinds) $ do foo <- resolveGenericCTree r modify @"synth" $ Map.insert fresh foo - else throwNR $ MismatchingArgs n params' - Nothing -> throwNR $ UnboundReference n + else throwNR $ MismatchingArgs (mapIndex n) params' + Nothing -> throwNR $ UnboundReference (mapIndex n) pure fresh resolveGenericRef :: XXType2 DistReferenced -> MonoM (TypeOrGroup MonoReferenced) -resolveGenericRef (RuleRef n []) = pure . CTreeE $ MRuleRef n +resolveGenericRef (RuleRef n []) = pure . undefined $ MRuleRef n resolveGenericRef (RuleRef n args) = do fresh <- synthMono n args - pure . CTreeE $ MRuleRef fresh + pure . TOGType . Type0 . NE.singleton $ Type1 (XXType2 $ MRuleRef fresh) Nothing mempty resolveGenericRef (GenericRef n) = do localBinds <- ask @"local" case Map.lookup n localBinds of Just node -> pure node Nothing -> throwNR $ UnboundReference n +resolveGenericRef (DistPostlude _) = undefined resolveGenericCTree :: TypeOrGroup DistReferenced -> MonoM (TypeOrGroup MonoReferenced) -resolveGenericCTree = CTree.traverseCTree resolveGenericRef resolveGenericCTree +resolveGenericCTree = undefined -- CTree.traverseCTree resolveGenericRef resolveGenericCTree data CTreeRoot i = CTreeRoot @@ -579,3 +581,54 @@ fullResolveCDDL cddl = do let refCTree = buildRefCTree (asMap cddl) rCTree <- buildResolvedCTree refCTree buildMonoCTree rCTree + +-- | +-- +-- CDDL predefines a number of names. This subsection summarizes these +-- names, but please see Appendix D for the exact definitions. +-- +-- The following keywords for primitive datatypes are defined: +-- +-- "bool" Boolean value (major type 7, additional information 20 +-- or 21). +-- +-- "uint" An unsigned integer (major type 0). +-- +-- "nint" A negative integer (major type 1). +-- +-- "int" An unsigned integer or a negative integer. +-- +-- "float16" A number representable as a half-precision float [IEEE754] +-- (major type 7, additional information 25). +-- +-- "float32" A number representable as a single-precision float +-- [IEEE754] (major type 7, additional information 26). +-- +-- +-- "float64" A number representable as a double-precision float +-- [IEEE754] (major type 7, additional information 27). +-- +-- "float" One of float16, float32, or float64. +-- +-- "bstr" or "bytes" A byte string (major type 2). +-- +-- "tstr" or "text" Text string (major type 3). +-- +-- (Note that there are no predefined names for arrays or maps; these +-- are defined with the syntax given below.) +data PTerm + = PTBool + | PTUInt + | PTNInt + | PTInt + | PTHalf + | PTFloat + | PTDouble + | PTBytes + | PTText + | PTAny + | PTNil + | PTUndefined + deriving (Eq, Generic, Ord, Show) + +instance Hashable PTerm diff --git a/src/Codec/CBOR/Cuddle/Pretty.hs b/src/Codec/CBOR/Cuddle/Pretty.hs index 5914fbf..c3fd984 100644 --- a/src/Codec/CBOR/Cuddle/Pretty.hs +++ b/src/Codec/CBOR/Cuddle/Pretty.hs @@ -29,7 +29,7 @@ import Data.List.NonEmpty qualified as NE import Data.String (IsString, fromString) import Data.Text qualified as T import Data.TreeDiff (ToExpr) -import Data.Void (Void, absurd) +import Data.Void (Void) import GHC.Generics (Generic) import Optics.Core ((^.)) import Prettyprinter