From 7e2b4e50a58315eb9f2e5f1926f37465ccfa4e55 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Mon, 13 Feb 2023 11:51:16 +0100 Subject: [PATCH 01/20] Drafted error messages --- lambda-buffers-proto/compiler-proto.md | 310 ++++++++++++++++++++++++- lambda-buffers-proto/compiler.proto | 63 ++++- 2 files changed, 358 insertions(+), 15 deletions(-) diff --git a/lambda-buffers-proto/compiler-proto.md b/lambda-buffers-proto/compiler-proto.md index 471269b5..5ab6541b 100644 --- a/lambda-buffers-proto/compiler-proto.md +++ b/lambda-buffers-proto/compiler-proto.md @@ -6,16 +6,30 @@ - [compiler.proto](#compiler-proto) - [ClassDef](#lambdabuffers-compiler-ClassDef) - [ClassName](#lambdabuffers-compiler-ClassName) + - [CompilerError](#lambdabuffers-compiler-CompilerError) - [CompilerInput](#lambdabuffers-compiler-CompilerInput) + - [CompilerOutput](#lambdabuffers-compiler-CompilerOutput) + - [CompilerResult](#lambdabuffers-compiler-CompilerResult) - [ConstrName](#lambdabuffers-compiler-ConstrName) - [Constraint](#lambdabuffers-compiler-Constraint) - [FieldName](#lambdabuffers-compiler-FieldName) - [InstanceClause](#lambdabuffers-compiler-InstanceClause) + - [InternalError](#lambdabuffers-compiler-InternalError) - [Kind](#lambdabuffers-compiler-Kind) - [Kind.KindArrow](#lambdabuffers-compiler-Kind-KindArrow) + - [KindCheckError](#lambdabuffers-compiler-KindCheckError) + - [KindCheckError.ImpossibleUnificationError](#lambdabuffers-compiler-KindCheckError-ImpossibleUnificationError) + - [KindCheckError.InconsistentTypeError](#lambdabuffers-compiler-KindCheckError-InconsistentTypeError) + - [KindCheckError.RecursiveKindError](#lambdabuffers-compiler-KindCheckError-RecursiveKindError) + - [KindCheckError.UnboundTermError](#lambdabuffers-compiler-KindCheckError-UnboundTermError) - [Module](#lambdabuffers-compiler-Module) - [ModuleName](#lambdabuffers-compiler-ModuleName) - [ModuleNamePart](#lambdabuffers-compiler-ModuleNamePart) + - [MultipleClassDefError](#lambdabuffers-compiler-MultipleClassDefError) + - [MultipleConstructorError](#lambdabuffers-compiler-MultipleConstructorError) + - [MultipleModuleError](#lambdabuffers-compiler-MultipleModuleError) + - [MultipleTyArgError](#lambdabuffers-compiler-MultipleTyArgError) + - [MultipleTyDefError](#lambdabuffers-compiler-MultipleTyDefError) - [NamingError](#lambdabuffers-compiler-NamingError) - [Opaque](#lambdabuffers-compiler-Opaque) - [Product](#lambdabuffers-compiler-Product) @@ -31,6 +45,9 @@ - [TyApp](#lambdabuffers-compiler-TyApp) - [TyArg](#lambdabuffers-compiler-TyArg) - [TyBody](#lambdabuffers-compiler-TyBody) + - [TyClassRef](#lambdabuffers-compiler-TyClassRef) + - [TyClassRef.Foreign](#lambdabuffers-compiler-TyClassRef-Foreign) + - [TyClassRef.Local](#lambdabuffers-compiler-TyClassRef-Local) - [TyDef](#lambdabuffers-compiler-TyDef) - [TyName](#lambdabuffers-compiler-TyName) - [TyRef](#lambdabuffers-compiler-TyRef) @@ -108,6 +125,27 @@ Type class name + + +### CompilerError +Compiler Error can be extended with other classes of errors. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| multiple_module_error | [MultipleModuleError](#lambdabuffers-compiler-MultipleModuleError) | | | +| multiple_tydef_error | [MultipleTyDefError](#lambdabuffers-compiler-MultipleTyDefError) | | | +| multiple_classdef_error | [MultipleClassDefError](#lambdabuffers-compiler-MultipleClassDefError) | | | +| multiple_tyarg_error | [MultipleTyArgError](#lambdabuffers-compiler-MultipleTyArgError) | | | +| multiple_constructor_error | [MultipleConstructorError](#lambdabuffers-compiler-MultipleConstructorError) | | | +| kind_check_error | [KindCheckError](#lambdabuffers-compiler-KindCheckError) | | | +| internal_error | [InternalError](#lambdabuffers-compiler-InternalError) | | | + + + + + + ### CompilerInput @@ -126,6 +164,34 @@ compilation closure needed by the Compiler to perform its task. + + +### CompilerOutput +Output of the Compiler. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| compilation_error | [CompilerError](#lambdabuffers-compiler-CompilerError) | | | +| compilation_result | [CompilerResult](#lambdabuffers-compiler-CompilerResult) | | | + + + + + + + + +### CompilerResult +Compiler Result ~ a successful Compilation Output. + +equivalent of unit. + + + + + + ### ConstrName @@ -150,7 +216,7 @@ Constraint expression | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| class_name | [ClassName](#lambdabuffers-compiler-ClassName) | | Name of the type class. | +| class_ref | [TyClassRef](#lambdabuffers-compiler-TyClassRef) | | Name of the type class. | | arguments | [Ty](#lambdabuffers-compiler-Ty) | repeated | Constraint arguments. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -185,7 +251,7 @@ Instance clauses enable users to specify 'semantic' rules for their type | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| class_name | [ClassName](#lambdabuffers-compiler-ClassName) | | Type class name. | +| class_ref | [TyClassRef](#lambdabuffers-compiler-TyClassRef) | | Type class name. | | heads | [Ty](#lambdabuffers-compiler-Ty) | repeated | Head of the instance clause. Currently, the Compiler only accepts single parameter type classes. | | constraints | [Constraint](#lambdabuffers-compiler-Constraint) | repeated | Body of the rule, conjunction of constraints. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -195,6 +261,21 @@ Instance clauses enable users to specify 'semantic' rules for their type + + +### InternalError +Internal errors. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| internal_error | [string](#string) | | | + + + + + + ### Kind @@ -210,7 +291,6 @@ etc. | ----- | ---- | ----- | ----------- | | kind_ref | [Kind.KindRef](#lambdabuffers-compiler-Kind-KindRef) | | | | kind_arrow | [Kind.KindArrow](#lambdabuffers-compiler-Kind-KindArrow) | | | -| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -233,6 +313,98 @@ A kind arrow. + + +### KindCheckError +Kind checking errors. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| unbound_term_error | [KindCheckError.UnboundTermError](#lambdabuffers-compiler-KindCheckError-UnboundTermError) | | | +| unification_error | [KindCheckError.ImpossibleUnificationError](#lambdabuffers-compiler-KindCheckError-ImpossibleUnificationError) | | | +| recursive_subs_error | [KindCheckError.RecursiveKindError](#lambdabuffers-compiler-KindCheckError-RecursiveKindError) | | | +| inconsistent_type_error | [KindCheckError.InconsistentTypeError](#lambdabuffers-compiler-KindCheckError-InconsistentTypeError) | | | + + + + + + + + +### KindCheckError.ImpossibleUnificationError +Unification has failed - type is incorrectly defined. Error reads as +follows: +> In ty_name definition an error has occurred when trying to unify kind +> ty_kind_1 with ty_kind_2. + +FIXME(cstml): add source of constraint to the error such that user can see +where the constraint was generated - therefore where the error precisely +is. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | | +| ty_kind_1 | [Kind](#lambdabuffers-compiler-Kind) | | | +| ty_kind_2 | [Kind](#lambdabuffers-compiler-Kind) | | | + + + + + + + + +### KindCheckError.InconsistentTypeError +The inferred type differs from the type as defined. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | | +| inferred_kind | [Kind](#lambdabuffers-compiler-Kind) | | | +| defined_kind | [Kind](#lambdabuffers-compiler-Kind) | | | + + + + + + + + +### KindCheckError.RecursiveKindError +Error reads: +Inifinitely recursive term detected in definition ty_name. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | | + + + + + + + + +### KindCheckError.UnboundTermError +Error referring to an unbound term. This usually means that the term was +not defined. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| ty_name | [TyName](#lambdabuffers-compiler-TyName) | | | +| var_name | [VarName](#lambdabuffers-compiler-VarName) | | | + + + + + + ### Module @@ -247,6 +419,7 @@ A module encapsulates type, class and instance definitions. | type_defs | [TyDef](#lambdabuffers-compiler-TyDef) | repeated | Type definitions. | | class_defs | [ClassDef](#lambdabuffers-compiler-ClassDef) | repeated | Type class definitions. | | instances | [InstanceClause](#lambdabuffers-compiler-InstanceClause) | repeated | Type class instance clauses. | +| imports | [ModuleName](#lambdabuffers-compiler-ModuleName) | repeated | Imported modules the Compiler consults when searching for instance clauses. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -286,6 +459,88 @@ Module name part + + +### MultipleClassDefError +Multiple ClassDefs with the same ClassName were found in ModuleName. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| class_defs | [ClassDef](#lambdabuffers-compiler-ClassDef) | repeated | Conflicting class definitions. | + + + + + + + + +### MultipleConstructorError +Multiple Sum Constructors with the same ConstrName were found in +ModuleName.TyDef. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | +| constructors | [Sum.Constructor](#lambdabuffers-compiler-Sum-Constructor) | repeated | Conflicting constructors. | + + + + + + + + +### MultipleModuleError +Multiple Modules with the same ModuleName were found. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| modules | [Module](#lambdabuffers-compiler-Module) | repeated | Conflicting type definitions. | + + + + + + + + +### MultipleTyArgError +Multiple TyArgs with the same ArgName were found in ModuleName.TyDef. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | +| ty_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | Conflicting type abstraction arguments. | + + + + + + + + +### MultipleTyDefError +Multiple TyDefs with the same TyName were found in ModuleName. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_defs | [TyDef](#lambdabuffers-compiler-TyDef) | repeated | Conflicting type definitions. | + + + + + + ### NamingError @@ -631,6 +886,55 @@ TODO: Add Tuple and Record type bodies. + + +### TyClassRef + + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| local_class_ref | [TyClassRef.Local](#lambdabuffers-compiler-TyClassRef-Local) | | | +| foreign_class_ref | [TyClassRef.Foreign](#lambdabuffers-compiler-TyClassRef-Foreign) | | | + + + + + + + + +### TyClassRef.Foreign +Foreign class reference. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| class_name | [ClassName](#lambdabuffers-compiler-ClassName) | | Foreign module class name. | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Foreign module name. | +| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | + + + + + + + + +### TyClassRef.Local +Local type reference. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| class_name | [ClassName](#lambdabuffers-compiler-ClassName) | | Local module class name. | +| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | + + + + + + ### TyDef diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index 2210cc53..afdb340c 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -529,7 +529,50 @@ message InternalError { string internal_error = 1; } -// Kindchecker errors. +// Multiple Modules with the same ModuleName were found. +message MultipleModuleError { + // Conflicting type definitions. + repeated Module modules = 2; +} + +// Multiple TyDefs with the same TyName were found in ModuleName. +message MultipleTyDefError { + // Module in which the error was found. + ModuleName module_name = 1; + // Conflicting type definitions. + repeated TyDef ty_defs = 2; +} + +// Multiple ClassDefs with the same ClassName were found in ModuleName. +message MultipleClassDefError { + // Module in which the error was found. + ModuleName module_name = 1; + // Conflicting class definitions. + repeated ClassDef class_defs = 2; +} + +// Multiple TyArgs with the same ArgName were found in ModuleName.TyDef. +message MultipleTyArgError { + // Module in which the error was found. + ModuleName module_name = 1; + // Type definition in which the error was found. + TyDef ty_def = 2; + // Conflicting type abstraction arguments. + repeated TyArg ty_args = 3; +} + +// Multiple Sum Constructors with the same ConstrName were found in +// ModuleName.TyDef. +message MultipleConstructorError { + // Module in which the error was found. + ModuleName module_name = 1; + // Type definition in which the error was found. + TyDef ty_def = 2; + // Conflicting constructors. + repeated Sum.Constructor constructors = 3; +} + +// Kind checking errors. message KindCheckError { // Error referring to an unbound term. This usually means that the term was @@ -566,21 +609,12 @@ message KindCheckError { Kind defined_kind = 3; } - // Multiple TyDefs with the same TyName were found in ModuleName. - message MultipleTyDefError { - // Module in which the error was found. - ModuleName module_name = 1; - // Conflicting type definitions. - repeated TyDef ty_defs = 2; - } - // The types of inference errors. oneof kind_check_error { UnboundTermError unbound_term_error = 1; ImpossibleUnificationError unification_error = 2; RecursiveKindError recursive_subs_error = 3; InconsistentTypeError inconsistent_type_error = 4; - MultipleTyDefError multiple_tydef_error = 5; } } @@ -589,8 +623,13 @@ message CompilerError { // Reason why the compilation failed. oneof compiler_error { - KindCheckError kind_check_error = 1; - InternalError internal_error = 3; + MultipleModuleError multiple_module_error = 1; + MultipleTyDefError multiple_tydef_error = 2; + MultipleClassDefError multiple_classdef_error = 3; + MultipleTyArgError multiple_tyarg_error = 4; + MultipleConstructorError multiple_constructor_error = 5; + KindCheckError kind_check_error = 6; + InternalError internal_error = 7; } } From aba79e4c08c07145d1ba2aaf20e77a81d75441bc Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Mon, 13 Feb 2023 12:19:42 +0100 Subject: [PATCH 02/20] Used MonadErro m --- .../src/LambdaBuffers/Compiler/ProtoCompat.hs | 36 +++++++------------ 1 file changed, 12 insertions(+), 24 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs index 64977716..60182723 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs @@ -15,6 +15,7 @@ module LambdaBuffers.Compiler.ProtoCompat ( import LambdaBuffers.Compiler.ProtoCompat.Types as X import Control.Lens (Getter, to, (&), (.~), (^.)) +import Control.Monad.Except (MonadError (throwError)) import Data.Foldable (toList) import Data.Generics.Labels () import Data.Kind (Type) @@ -29,11 +30,6 @@ import Proto.Compiler (NamingError) import Proto.Compiler qualified as P import Proto.Compiler_Fields qualified as P -note :: e -> Maybe a -> Either e a -note e = \case - Nothing -> Left e - Just a -> Right a - -- FIXME(bladyjoker): This emits a missing Functor constraint @gnumonik -- something like this probably exists in lens but i can't find it traversing :: (Traversable t, Applicative f) => (a -> f b) -> Getter (t a) (f (t b)) @@ -45,12 +41,12 @@ data FromProtoErr deriving stock (Show, Eq, Ord, Generic) class IsMessage (proto :: Type) (good :: Type) where - fromProto :: proto -> Either FromProtoErr good + fromProto :: MonadError FromProtoErr m => proto -> m good toProto :: good -> proto -throwNamingError :: Either NamingError b -> Either FromProtoErr b -throwNamingError = either (Left . NamingError) return +throwNamingError :: MonadError FromProtoErr m => Either NamingError b -> m b +throwNamingError = either (throwError . NamingError) return -- TODO(bladyjoker): Revisit and make part of compiler.proto data ProtoError @@ -69,8 +65,8 @@ data ProtoError | UnrecognizedKindRefEnum Text deriving stock (Show, Eq, Ord) -throwProtoError :: ProtoError -> Either FromProtoErr b -throwProtoError = Left . ProtoError +throwProtoError :: MonadError FromProtoErr m => ProtoError -> m b +throwProtoError = throwError . ProtoError {- SourceInfo @@ -170,7 +166,7 @@ instance IsMessage P.TyApp TyApp where tf <- fromProto $ ta ^. P.tyFunc si <- fromProto $ ta ^. P.sourceInfo targs' <- ta ^. (P.tyArgs . traversing fromProto) - targs <- note (ProtoError $ NoTyAppArgs si) $ nonEmpty targs' + targs <- maybe (throwProtoError $ NoTyAppArgs si) return $ nonEmpty targs' pure $ TyApp tf targs si toProto (TyApp tf args si) = @@ -314,7 +310,7 @@ instance IsMessage P.Sum Sum where fromProto s = do si <- fromProto $ s ^. P.sourceInfo ctors' <- s ^. (P.constructors . traversing fromProto) - ctors <- note (ProtoError $ EmptySumBody si) $ nonEmpty ctors' + ctors <- maybe (throwProtoError $ EmptySumBody si) return $ nonEmpty ctors' pure $ Sum ctors si toProto (Sum ctors si) = @@ -337,7 +333,7 @@ instance IsMessage P.Product'Record Record where fromProto r = do fs' <- traverse fromProto $ r ^. P.fields si <- fromProto $ r ^. P.sourceInfo - fs <- note (ProtoError $ EmptyRecordBody si) $ nonEmpty fs' + fs <- maybe (throwProtoError $ EmptyRecordBody si) return $ nonEmpty fs' pure $ Record fs si toProto (Record fs si) = @@ -429,7 +425,7 @@ instance IsMessage P.ClassDef ClassDef where cargs <- traverse fromProto $ cd ^. P.classArgs carg <- case cargs of [] -> throwProtoError $ NoClassArgs cnm si - [x] -> Right x + [x] -> return x _ -> throwProtoError $ MultipleClassArgs cnm si sups <- traverse fromProto $ cd ^. P.supers let doc = cd ^. P.documentation @@ -451,7 +447,7 @@ instance IsMessage P.InstanceClause InstanceClause where hds <- ic ^. (P.heads . traversing fromProto) hd <- case hds of [] -> throwProtoError $ NoInstanceHead cnm si - [x] -> Right x + [x] -> return x xs -> throwProtoError $ MultipleInstanceHeads cnm xs si pure $ InstanceClause cnm hd csts si @@ -469,7 +465,7 @@ instance IsMessage P.Constraint Constraint where args <- c ^. (P.arguments . traversing fromProto) arg <- case args of [] -> throwProtoError $ NoConstraintArgs cnm si - [x] -> Right x + [x] -> return x xs -> throwProtoError $ MultipleConstraintArgs cnm xs si pure $ Constraint cnm arg si @@ -566,10 +562,6 @@ instance IsMessage P.KindCheckError KindCheckError where <$> fromProto (err ^. P.tyName) <*> fromProto (err ^. P.inferredKind) <*> fromProto (err ^. P.definedKind) - P.KindCheckError'MultipleTydefError err -> - MultipleTyDefError - <$> fromProto (err ^. P.moduleName) - <*> traverse fromProto (err ^. P.tyDefs) Nothing -> throwProtoError EmptyField toProto = \case @@ -590,10 +582,6 @@ instance IsMessage P.KindCheckError KindCheckError where & (P.inconsistentTypeError . P.tyName) .~ toProto name & (P.inconsistentTypeError . P.inferredKind) .~ toProto ki & (P.inconsistentTypeError . P.definedKind) .~ toProto kd - MultipleTyDefError m ds -> - defMessage - & (P.multipleTydefError . P.moduleName) .~ toProto m - & (P.multipleTydefError . P.tyDefs) .~ (toProto <$> ds) instance IsMessage P.CompilerError CompilerError where fromProto cErr = case cErr ^. P.maybe'compilerError of From 7e2378d70c335d1438eea0f3f641f815922c7275 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Mon, 13 Feb 2023 18:20:33 +0000 Subject: [PATCH 03/20] update: KC 1 constructor at a time + add Variable in inference --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 80 +++++++++++++------ .../Compiler/KindCheck/Inference.hs | 2 +- 2 files changed, 58 insertions(+), 24 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 927fd829..fd5da4e1 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -19,7 +19,10 @@ import Control.Monad.Freer.Reader (Reader, ask, runReader) import Control.Monad.Freer.State (State, evalState, get, modify) import Control.Monad.Freer.TH (makeEffect) import Data.Foldable (traverse_) +import Data.Functor ((<&>)) import Data.List.NonEmpty (NonEmpty ((:|)), uncons, (<|)) +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map (Map) import Data.Map qualified as M import Data.Text (Text, intercalate) import LambdaBuffers.Compiler.KindCheck.Context (Context) @@ -68,19 +71,19 @@ makeEffect ''GlobalCheck -- | Interactions that happen at the level of the data ModuleCheck a where -- Module KCTypeDefinition :: ModName -> Context -> P.TyDef -> ModuleCheck Kind - KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck () - KCClass :: Context -> P.ClassDef -> ModuleCheck () + +-- fixme(cstml & gnumonik): lets reach consensus on these - Note(1). +-- KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck () +-- KCClass :: Context -> P.ClassDef -> ModuleCheck () makeEffect ''ModuleCheck data KindCheck a where - KindFromTyDef :: ModName -> P.TyDef -> KindCheck Type + -- TypeFromTyDef :: ModName -> P.TyDef -> KindCheck Type -- replaced with constructor by constructor check + TypesFromTyDef :: ModName -> P.TyDef -> KindCheck [Type] -- each constructor is a Type Term which gets checked InferTypeKind :: ModName -> P.TyDef -> Context -> Type -> KindCheck Kind CheckKindConsistency :: ModName -> P.TyDef -> Context -> Kind -> KindCheck Kind --- FIXME(cstml) add check for Context Consistency --- FIXME(cstml) add check for Double Declaration --- TyDefToTypes :: ModName -> P.TyDef -> KindCheck [Type] makeEffect ''KindCheck -------------------------------------------------------------------------------- @@ -120,20 +123,31 @@ moduleStrategy = reinterpret $ \case CreateContext ci -> evalState (mempty @(M.Map Variable P.TyDef)) . resolveCreateContext $ ci ValidateModule cx md -> do traverse_ (kCTypeDefinition (module2ModuleName md) cx) (md ^. #typeDefs) - traverse_ (kCClassInstance cx) (md ^. #instances) - traverse_ (kCClass cx) (md ^. #classDefs) +{- See note (1). +-- traverse_ (kCClassInstance cx) (md ^. #instances) -- fixme(cstml): not implemented to discuss with Sean. +-- traverse_ (kCClass cx) (md ^. #classDefs) +-} localStrategy :: Transform ModuleCheck KindCheck localStrategy = reinterpret $ \case KCTypeDefinition mname ctx tydef -> do - kindFromTyDef mname tydef >>= inferTypeKind mname tydef ctx >>= checkKindConsistency mname tydef ctx - KCClassInstance _ctx _instClause -> pure () -- "FIXME(cstml)" - KCClass _ctx _classDef -> pure () -- "FIXME(cstml)" + typesFromTyDef mname tydef + >>= traverse (inferTypeKind mname tydef ctx) + >>= traverse (checkKindConsistency mname tydef ctx) + >>= traverse (checkKindConsistency mname tydef ctx) + >>= \case + [] -> pure Type -- Void + x : _ -> pure x -- The Kind of the first constructor ~ already checked + -- and consistent. + {- See note (1). + -- KCClassInstance _ctx _instClause -> pure () + -- KCClass _ctx _classDef -> pure () + -} runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a runKindCheck = interpret $ \case - KindFromTyDef moduleName tydef -> runReader moduleName (tyDef2Type tydef) - -- TyDefToTypes moduleName tydef -> runReader moduleName (tyDef2Types tydef) + -- TypeFromTyDef moduleName tydef -> runReader moduleName (tyDef2Type tydef) + TypesFromTyDef moduleName tydef -> runReader moduleName (tyDef2Types tydef) InferTypeKind _modName tyDef ctx ty -> either (handleErr tyDef) pure $ infer ctx ty CheckKindConsistency mname def ctx k -> runReader mname $ resolveKindConsistency def ctx k where @@ -221,8 +235,9 @@ tyDef2Context :: Eff effs Context tyDef2Context curModName tyDef = do r@(v, _) <- tyDef2NameAndKind curModName tyDef + ctx2 <- tyDefArgs2Context tyDef associateName v tyDef - pure $ mempty & context .~ uncurry M.singleton r + pure $ mempty & context .~ uncurry M.singleton r <> ctx2 where -- Ads the name to our map - we can use its SourceLocation in the case of a -- double use. If it's already in our map - that means we've double declared it. @@ -235,6 +250,20 @@ tyDef2Context curModName tyDef = do throwError . PT.CompKindCheckError $ PT.MultipleTyDefError modName [otherTyDef, curTyDef] Nothing -> modify (M.insert v curTyDef) +{- | Gets the kind of the variables from the definition and adds them to the + context. +-} +tyDefArgs2Context :: P.TyDef -> Eff effs (Map Variable Kind) +tyDefArgs2Context tydef = do + let ds = g <$> (tydef ^. #tyAbs . #tyArgs) + pure $ M.fromList ds + where + g :: PT.TyArg -> (Variable, Kind) + g tyarg = (v, k) + where + v = LocalRef (tyarg ^. #argName . #name) + k = pKind2Kind (tyarg ^. #argKind) + {- | Converts the Proto Module name to a local modname - dropping the information. -} @@ -249,7 +278,7 @@ tyDef2NameAndKind curModName tyDef = do pure (name, k) tyAbsLHS2Kind :: P.TyAbs -> Kind -tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs) +tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Kind . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs) foldWithArrow :: [Kind] -> Kind foldWithArrow = foldl (:->:) Type @@ -257,17 +286,17 @@ foldWithArrow = foldl (:->:) Type -- ================================================================================ -- To Kind Conversion functions -pKind2Type :: P.Kind -> Kind -pKind2Type k = +pKind2Kind :: P.Kind -> Kind +pKind2Kind k = case k ^. #kind of P.KindRef P.KType -> Type - P.KindArrow l r -> pKind2Type l :->: pKind2Type r + P.KindArrow l r -> pKind2Kind l :->: pKind2Kind r -- FIXME(cstml) what is an undefined type meant to mean? _ -> error "Fixme undefined type" -- ============================================================================= -- X To Canonical type conversion functions. - +{- Replaced with Constructor by Constructor check. -- | TyDef to Kind Canonical representation. tyDef2Type :: forall eff. @@ -275,7 +304,7 @@ tyDef2Type :: P.TyDef -> Eff eff Type tyDef2Type tyde = tyAbsLHS2Type (tyde ^. #tyAbs) <*> tyAbsRHS2Type (tyde ^. #tyAbs) - +-} tyAbsLHS2Type :: forall eff. P.TyAbs -> @@ -295,6 +324,7 @@ tyArgs2Type = \case tyArg2Var :: P.TyArg -> Variable tyArg2Var = LocalRef . view (#argName . #name) +{- Replaced with Constructor by Constructor check. tyAbsRHS2Type :: forall eff. Members '[Reader ModName, Err] eff => @@ -317,6 +347,7 @@ sum2Type :: P.Sum -> Eff eff Type sum2Type su = foldWithSum <$> traverse constructor2Type (su ^. #constructors) +-} constructor2Type :: forall eff. @@ -413,8 +444,11 @@ foreignTyRef2Type ftr = do -- ============================================================================= -- X To Canonical type conversion functions. -{- --- | TyDef to Kind Canonical representation - sums not folded - therefore we get constructor granularity. Might use in a different implementation for more granular errors. + +{- | TyDef to Kind Canonical representation - sums not folded - therefore we get + constructor granularity. Might use in a different implementation for more + granular errors. +-} tyDef2Types :: forall eff. Members '[Reader ModName, Err] eff => @@ -447,7 +481,7 @@ sum2Types :: P.Sum -> Eff eff [Type] sum2Types su = NonEmpty.toList <$> traverse constructor2Type (su ^. #constructors) --} + -------------------------------------------------------------------------------- -- Utilities diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 11bc8d76..debab97c 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -122,7 +122,7 @@ derive x = do tell [Constraint (ty1, ty2 :->: v)] pure $ Application (Judgement (c, x, v)) d1 d2 Abs v t -> do - newTy <- KVar <$> fresh + newTy <- getBinding v d <- local (\(Context ctx addC) -> Context ctx $ M.insert v newTy addC) (derive t) let ty = d ^. topKind freshT <- KVar <$> fresh From 097f048a76ae5877ed1adaf1561c580e379f4010 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Mon, 13 Feb 2023 18:29:23 +0000 Subject: [PATCH 04/20] lint: remove redundant import --- lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index fd5da4e1..1017049e 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -19,7 +19,6 @@ import Control.Monad.Freer.Reader (Reader, ask, runReader) import Control.Monad.Freer.State (State, evalState, get, modify) import Control.Monad.Freer.TH (makeEffect) import Data.Foldable (traverse_) -import Data.Functor ((<&>)) import Data.List.NonEmpty (NonEmpty ((:|)), uncons, (<|)) import Data.List.NonEmpty qualified as NonEmpty import Data.Map (Map) From e6e7bfdfcf418d73a715c86e2cbaf7a30cc997f2 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Mon, 13 Feb 2023 19:31:05 +0100 Subject: [PATCH 05/20] Saved work, tests almost working --- .../lambda-buffers-compiler.cabal | 1 + .../src/LambdaBuffers/Compiler/KindCheck.hs | 53 ++-- .../Compiler/KindCheck/Inference.hs | 12 +- .../LambdaBuffers/Compiler/KindCheck/Type.hs | 20 ++ .../src/LambdaBuffers/Compiler/NamingCheck.hs | 38 ++- .../src/LambdaBuffers/Compiler/ProtoCompat.hs | 226 ++++++++++++------ .../Compiler/ProtoCompat/Types.hs | 20 +- .../test/Test/KindCheck.hs | 55 +++-- .../test/Test/Utils/CompilerInput.hs | 8 +- .../test/Test/Utils/Constructors.hs | 18 +- .../test/Test/Utils/Module.hs | 21 +- lambda-buffers-proto/compiler.proto | 175 ++++++++------ 12 files changed, 380 insertions(+), 267 deletions(-) diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index df34ff31..0add5645 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -148,6 +148,7 @@ test-suite tests hs-source-dirs: test main-is: Test.hs build-depends: + , containers >=0.6 , lambda-buffers-compiler , lambda-buffers-compiler-pb >=0.1 , proto-lens >=0.7 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 927fd829..bc48f8d3 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -18,8 +18,7 @@ import Control.Monad.Freer.Error (Error, runError, throwError) import Control.Monad.Freer.Reader (Reader, ask, runReader) import Control.Monad.Freer.State (State, evalState, get, modify) import Control.Monad.Freer.TH (makeEffect) -import Data.Foldable (traverse_) -import Data.List.NonEmpty (NonEmpty ((:|)), uncons, (<|)) +import Data.Foldable (Foldable (foldl', toList), traverse_) import Data.Map qualified as M import Data.Text (Text, intercalate) import LambdaBuffers.Compiler.KindCheck.Context (Context) @@ -36,7 +35,7 @@ import LambdaBuffers.Compiler.KindCheck.Inference ( infer, ) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I -import LambdaBuffers.Compiler.KindCheck.Type (Type (App)) +import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyEither, tyOpaque, tyProd, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef)) import LambdaBuffers.Compiler.ProtoCompat (kind2ProtoKind) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P @@ -79,7 +78,6 @@ data KindCheck a where CheckKindConsistency :: ModName -> P.TyDef -> Context -> Kind -> KindCheck Kind -- FIXME(cstml) add check for Context Consistency --- FIXME(cstml) add check for Double Declaration -- TyDefToTypes :: ModName -> P.TyDef -> KindCheck [Type] makeEffect ''KindCheck @@ -195,7 +193,7 @@ resolveCreateContext :: P.CompilerInput -> Eff effs Context resolveCreateContext ci = do - ctxs <- traverse module2Context (ci ^. #modules) + ctxs <- traverse module2Context (toList $ ci ^. #modules) pure $ mconcat ctxs module2Context :: @@ -205,7 +203,7 @@ module2Context :: P.Module -> Eff effs Context module2Context m = do - let typeDefinitions = m ^. #typeDefs + let typeDefinitions = toList $ m ^. #typeDefs ctxs <- runReader (m ^. #moduleName) $ do traverse (tyDef2Context (moduleName2ModName (m ^. #moduleName))) typeDefinitions pure $ mconcat ctxs @@ -249,7 +247,7 @@ tyDef2NameAndKind curModName tyDef = do pure (name, k) tyAbsLHS2Kind :: P.TyAbs -> Kind -tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> (tyAbs ^. #tyArgs) +tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs) foldWithArrow :: [Kind] -> Kind foldWithArrow = foldl (:->:) Type @@ -265,10 +263,9 @@ pKind2Type k = -- FIXME(cstml) what is an undefined type meant to mean? _ -> error "Fixme undefined type" --- ============================================================================= --- X To Canonical type conversion functions. - --- | TyDef to Kind Canonical representation. +{- | TyDef to Kind Canonical representation. + TODO(@cstml): Move this close to KindCheck/Type.hs (even just there). +-} tyDef2Type :: forall eff. Members '[Reader ModName, Err] eff => @@ -280,7 +277,7 @@ tyAbsLHS2Type :: forall eff. P.TyAbs -> Eff eff (Type -> Type) -tyAbsLHS2Type tyab = tyArgs2Type (tyab ^. #tyArgs) +tyAbsLHS2Type tyab = tyArgs2Type (toList $ tyab ^. #tyArgs) tyArgs2Type :: forall eff. @@ -308,7 +305,7 @@ tyBody2Type :: P.TyBody -> Eff eff Type tyBody2Type = \case - P.OpaqueI _ -> pure $ Var $ LocalRef "Opaque" + P.OpaqueI _ -> pure $ Var tyOpaque P.SumI s -> sum2Type s sum2Type :: @@ -316,7 +313,7 @@ sum2Type :: Members '[Reader ModName, Err] eff => P.Sum -> Eff eff Type -sum2Type su = foldWithSum <$> traverse constructor2Type (su ^. #constructors) +sum2Type su = foldWithSum <$> traverse constructor2Type (toList $ su ^. #constructors) constructor2Type :: forall eff. @@ -339,7 +336,7 @@ record2Type :: Members '[Reader ModName, Err] eff => P.Record -> Eff eff Type -record2Type r = foldWithProduct <$> traverse field2Type (r ^. #fields) +record2Type r = foldWithProduct <$> traverse field2Type (toList $ r ^. #fields) tuple2Type :: forall eff. @@ -348,9 +345,7 @@ tuple2Type :: Eff eff Type tuple2Type tu = do tup <- traverse ty2Type $ tu ^. #fields - case tup of - [] -> pure $ Var $ LocalRef "𝟙" - x : xs -> pure . foldWithProduct $ x :| xs + pure . foldWithProduct $ tup field2Type :: forall eff. @@ -382,8 +377,8 @@ tyApp2Type :: Eff eff Type tyApp2Type ta = do fn <- ty2Type (ta ^. #tyFunc) - args <- traverse ty2Type (ta ^. #tyArgs) - pure $ foldWithApp (fn <| args) + args <- traverse ty2Type (toList $ ta ^. #tyArgs) + pure $ foldWithApp fn args tyRef2Type :: forall eff. @@ -451,20 +446,14 @@ sum2Types su = NonEmpty.toList <$> traverse constructor2Type (su ^. #constructor -------------------------------------------------------------------------------- -- Utilities -foldWithApp :: NonEmpty Type -> Type -foldWithApp = foldWithBinaryOp App - -foldWithProduct :: NonEmpty Type -> Type -foldWithProduct = foldWithBinaryOp $ App . App (Var $ LocalRef "Π") +foldWithApp :: Type -> [Type] -> Type +foldWithApp = foldl' App -foldWithSum :: NonEmpty Type -> Type -foldWithSum = foldWithBinaryOp $ App . App (Var $ LocalRef "Σ") +foldWithProduct :: [Type] -> Type +foldWithProduct = foldl' (App . App (Var tyProd)) (Var tyUnit) --- | Generic way of folding. -foldWithBinaryOp :: (Type -> Type -> Type) -> NonEmpty Type -> Type -foldWithBinaryOp op ne = case uncons ne of - (x, Nothing) -> x - (x, Just xs) -> op x $ foldWithBinaryOp op xs +foldWithSum :: [Type] -> Type +foldWithSum = foldl' (App . App (Var tyEither)) (Var tyVoid) module2ModuleName :: P.Module -> ModName module2ModuleName = moduleName2ModName . (^. #moduleName) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 11bc8d76..42db734e 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -21,8 +21,8 @@ import LambdaBuffers.Compiler.KindCheck.Context (Context (Context), addContext, import LambdaBuffers.Compiler.KindCheck.Derivation (Derivation (Abstraction, Application, Axiom)) import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement (Judgement)) import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KVar, Type, (:->:))) -import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var)) -import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable (LocalRef)) +import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyEither, tyProd, tyUnit, tyVoid) +import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable) import Control.Monad.Freer (Eff, Member, Members, run) import Control.Monad.Freer.Error (Error, runError, throwError) @@ -96,10 +96,10 @@ infer ctx t = do mempty & context .~ M.fromList - [ (LocalRef "Σ", Type :->: Type :->: Type) - , (LocalRef "Π", Type :->: Type :->: Type) - , (LocalRef "𝟙", Type) - , (LocalRef "𝟘", Type) + [ (tyEither, Type :->: Type :->: Type) + , (tyProd, Type :->: Type :->: Type) + , (tyUnit, Type) + , (tyVoid, Type) ] -------------------------------------------------------------------------------- diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs index 201f855f..3a84731d 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs @@ -4,6 +4,11 @@ module LambdaBuffers.Compiler.KindCheck.Type ( Type (Var, Abs, App), pattern Σ, pattern Π, + tyOpaque, + tyUnit, + tyVoid, + tyEither, + tyProd, ) where import LambdaBuffers.Compiler.KindCheck.Variable (Variable (LocalRef)) @@ -16,6 +21,21 @@ data Type | Abs Variable Type deriving stock (Eq, Show) +tyOpaque :: Variable +tyOpaque = LocalRef "Opaque" + +tyUnit :: Variable +tyUnit = LocalRef "𝟙" + +tyVoid :: Variable +tyVoid = LocalRef "𝟘" + +tyEither :: Variable +tyEither = LocalRef "Σ" + +tyProd :: Variable +tyProd = LocalRef "Π" + pattern Σ :: Type -> Type -> Type pattern Σ t1 t2 = App (App (Var (LocalRef "Σ")) t1) t2 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs index 460f73bf..3a7338c5 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs @@ -1,6 +1,6 @@ module LambdaBuffers.Compiler.NamingCheck (pModuleNamePart, pVarName, pTyName, pConstrName, pFieldName, pClassName, checkModuleName, checkTyName, checkVarName, checkConstrName, checkClassName, checkFieldName) where -import Control.Lens ((.~), (^.)) +import Control.Lens (ASetter, (.~), (^.)) import Control.Monad.Except (MonadError (throwError)) import Data.Foldable (for_) import Data.Function ((&)) @@ -9,8 +9,8 @@ import Data.ProtoLens (Message (defMessage)) import Data.ProtoLens.Field (HasField) import Data.String (IsString (fromString)) import Data.Text (Text) -import Proto.Compiler (ClassName, ConstrName, FieldName, Module, NamingError, NamingError'NameType (NamingError'NAME_TYPE_CLASS, NamingError'NAME_TYPE_CONSTR, NamingError'NAME_TYPE_FIELD, NamingError'NAME_TYPE_MODULE, NamingError'NAME_TYPE_TYPE, NamingError'NAME_TYPE_VAR), SourceInfo, TyName, VarName) -import Proto.Compiler_Fields (moduleName, name, nameType, parts, sourceInfo) +import Proto.Compiler (ClassName, ConstrName, FieldName, Module, NamingError, TyName, VarName) +import Proto.Compiler_Fields (classNameErr, constrNameErr, fieldNameErr, moduleName, moduleNameErr, name, parts, tyNameErr, varNameErr) import Text.Parsec (ParsecT, Stream, alphaNum, label, lower, many, many1, runParserT) import Text.Parsec.Char (upper) @@ -45,38 +45,34 @@ label' :: String -> Parser s m a -> Parser s m a label' l m = label m l validateP :: - ( MonadError NamingError m - , HasField a "sourceInfo" SourceInfo - , HasField a "name" Text - ) => + (HasField i "name" Text, MonadError NamingError m, Message a1) => Parser Text m Text -> - NamingError'NameType -> - a -> + ASetter a1 NamingError a3 i -> + i -> m () -validateP p nt i = do +validateP p f i = do resOrErr <- runParserT p () "" (i ^. name) case resOrErr of - Left _ -> - throwError $ - defMessage - & nameType .~ nt - & sourceInfo .~ (i ^. sourceInfo) + Left _ -> throwError $ defMessage & f .~ i Right _ -> return () checkModuleName :: MonadError NamingError m => Module -> m () -checkModuleName m = for_ (m ^. (moduleName . parts)) (validateP pModuleNamePart NamingError'NAME_TYPE_MODULE) +checkModuleName m = + for_ + (m ^. (moduleName . parts)) + (validateP pModuleNamePart moduleNameErr) checkTyName :: MonadError NamingError m => TyName -> m () -checkTyName = validateP pTyName NamingError'NAME_TYPE_TYPE +checkTyName = validateP pTyName tyNameErr checkVarName :: MonadError NamingError m => VarName -> m () -checkVarName = validateP pVarName NamingError'NAME_TYPE_VAR +checkVarName = validateP pVarName varNameErr checkConstrName :: MonadError NamingError m => ConstrName -> m () -checkConstrName = validateP pConstrName NamingError'NAME_TYPE_CONSTR +checkConstrName = validateP pConstrName constrNameErr checkFieldName :: MonadError NamingError m => FieldName -> m () -checkFieldName = validateP pFieldName NamingError'NAME_TYPE_FIELD +checkFieldName = validateP pFieldName fieldNameErr checkClassName :: MonadError NamingError m => ClassName -> m () -checkClassName = validateP pClassName NamingError'NAME_TYPE_CLASS +checkClassName = validateP pClassName classNameErr diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs index 60182723..b36ed9d8 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs @@ -12,15 +12,18 @@ module LambdaBuffers.Compiler.ProtoCompat ( -- NOTE(cstml): I'm re-exporting the module from here as it makes more sense - -- also avoids annoying errors. -import LambdaBuffers.Compiler.ProtoCompat.Types as X +import LambdaBuffers.Compiler.ProtoCompat.Types as X hiding (InternalError) import Control.Lens (Getter, to, (&), (.~), (^.)) import Control.Monad.Except (MonadError (throwError)) -import Data.Foldable (toList) +import Data.Foldable (foldlM, toList) import Data.Generics.Labels () import Data.Kind (Type) -import Data.List.NonEmpty (nonEmpty) -import Data.ProtoLens (defMessage) +import Data.Map (Map) +import Data.Map qualified as Map +import Data.ProtoLens (Message (messageName), defMessage) +import Data.Proxy (Proxy (Proxy)) +import Data.Set qualified as Set import Data.Text (Text) import Data.Text qualified as Text import GHC.Generics (Generic) @@ -37,17 +40,18 @@ traversing f = to $ \ta -> traverse f ta data FromProtoErr = ProtoError ProtoError - | NamingError NamingError + | NamingError P.NamingError + | InternalError P.InternalError + | ProtoParseError P.ProtoParseError deriving stock (Show, Eq, Ord, Generic) +type FromProto a = forall m. MonadError [FromProtoErr] m => m a + class IsMessage (proto :: Type) (good :: Type) where - fromProto :: MonadError FromProtoErr m => proto -> m good + fromProto :: proto -> FromProto good toProto :: good -> proto -throwNamingError :: MonadError FromProtoErr m => Either NamingError b -> m b -throwNamingError = either (throwError . NamingError) return - -- TODO(bladyjoker): Revisit and make part of compiler.proto data ProtoError = MultipleInstanceHeads TyClassRef [Ty] SourceInfo @@ -56,17 +60,27 @@ data ProtoError | MultipleConstraintArgs TyClassRef [Ty] SourceInfo | NoClassArgs ClassName SourceInfo | MultipleClassArgs ClassName SourceInfo - | NoTyAppArgs SourceInfo - | EmptyRecordBody SourceInfo -- Ideally we should catch & rethrow this and the next one when we have access to the tyname - | EmptySumBody SourceInfo - | EmptyName SourceInfo | EmptyField - | OneOfNotSet Text | UnrecognizedKindRefEnum Text deriving stock (Show, Eq, Ord) -throwProtoError :: MonadError FromProtoErr m => ProtoError -> m b -throwProtoError = throwError . ProtoError +throwNamingError :: Either NamingError b -> FromProto b +throwNamingError = either (\err -> throwError [NamingError err]) return + +throwOneOfError :: Text -> Text -> FromProto b +throwOneOfError protoMsgName protoFieldName = + throwError + [ ProtoParseError $ + defMessage + & P.oneOfNotSetError . P.messageName .~ protoMsgName + & P.oneOfNotSetError . P.fieldName .~ protoFieldName + ] + +throwProtoError :: ProtoError -> FromProto b +throwProtoError err = throwError [ProtoError err] + +throwInternalError :: Text -> FromProto b +throwInternalError msg = throwError [InternalError $ defMessage & P.msg .~ msg] {- SourceInfo @@ -165,8 +179,7 @@ instance IsMessage P.TyApp TyApp where fromProto ta = do tf <- fromProto $ ta ^. P.tyFunc si <- fromProto $ ta ^. P.sourceInfo - targs' <- ta ^. (P.tyArgs . traversing fromProto) - targs <- maybe (throwProtoError $ NoTyAppArgs si) return $ nonEmpty targs' + targs <- ta ^. (P.tyArgs . traversing fromProto) pure $ TyApp tf targs si toProto (TyApp tf args si) = @@ -177,7 +190,7 @@ instance IsMessage P.TyApp TyApp where instance IsMessage P.Ty Ty where fromProto ti = case ti ^. P.maybe'ty of - Nothing -> throwProtoError $ OneOfNotSet "ty" + Nothing -> throwOneOfError (messageName (Proxy @P.Ty)) "ty" Just x -> case x of P.Ty'TyVar tv -> TyVarI <$> fromProto tv P.Ty'TyApp ta -> TyAppI <$> fromProto ta @@ -214,7 +227,7 @@ instance IsMessage P.TyRef'Foreign ForeignRef where instance IsMessage P.TyRef TyRef where fromProto tr = case tr ^. P.maybe'tyRef of - Nothing -> throwProtoError $ OneOfNotSet "ty_ref" + Nothing -> throwOneOfError (messageName (Proxy @P.TyRef)) "ty_ref" Just x -> case x of P.TyRef'LocalTyRef lr -> LocalI <$> fromProto lr P.TyRef'ForeignTyRef f -> ForeignI <$> fromProto f @@ -242,14 +255,23 @@ instance IsMessage P.TyDef TyDef where instance IsMessage P.TyAbs TyAbs where fromProto ta = do - tyvars <- traverse fromProto $ ta ^. P.tyArgs + (tyargs, mulTyArgs) <- collectMultipleKeys (\a -> a ^. #argName) (ta ^. P.tyArgs) tybody <- fromProto $ ta ^. P.tyBody si <- fromProto $ ta ^. P.sourceInfo - pure $ TyAbs tyvars tybody si - - toProto (TyAbs tyvars tyabs si) = + let mulArgsErrs = + [ ProtoParseError $ + defMessage + -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleTyargError . P.tyArgs .~ args + | (_an, args) <- Map.toList mulTyArgs + ] + if null mulArgsErrs + then pure $ TyAbs tyargs tybody si + else throwError mulArgsErrs + + toProto (TyAbs tyargs tyabs si) = defMessage - & P.tyArgs .~ (toProto <$> tyvars) + & P.tyArgs .~ (toProto <$> toList tyargs) & P.tyBody .~ toProto tyabs & P.sourceInfo .~ toProto si @@ -266,7 +288,7 @@ instance IsMessage P.Kind'KindRef KindRefType where instance IsMessage P.Kind Kind where fromProto k = do kt <- case k ^. P.maybe'kind of - Nothing -> throwProtoError $ OneOfNotSet "ty_ref" + Nothing -> throwOneOfError (messageName (Proxy @P.Kind)) "kind" Just k' -> case k' of P.Kind'KindRef r -> KindRef <$> fromProto r P.Kind'KindArrow' arr -> KindArrow <$> fromProto (arr ^. P.left) <*> fromProto (arr ^. P.right) @@ -295,7 +317,7 @@ instance IsMessage P.TyArg TyArg where instance IsMessage P.TyBody TyBody where fromProto tb = case tb ^. P.maybe'tyBody of - Nothing -> throwProtoError $ OneOfNotSet "tyBody" + Nothing -> throwOneOfError (messageName (Proxy @P.TyBody)) "ty_body" Just x -> case x of P.TyBody'Opaque opq -> OpaqueI <$> fromProto (opq ^. P.sourceInfo) P.TyBody'Sum sumI -> SumI <$> fromProto sumI @@ -308,10 +330,19 @@ instance IsMessage P.TyBody TyBody where instance IsMessage P.Sum Sum where fromProto s = do + (ctors, mulCtors) <- collectMultipleKeys (\c -> c ^. #constrName) (s ^. P.constructors) si <- fromProto $ s ^. P.sourceInfo - ctors' <- s ^. (P.constructors . traversing fromProto) - ctors <- maybe (throwProtoError $ EmptySumBody si) return $ nonEmpty ctors' - pure $ Sum ctors si + -- TODO(bladyjoker): ctors <- maybe (throwProtoError $ EmptySumBody si) return $ nonEmpty ctors' + let mulFieldsErrs = + [ ProtoParseError $ + defMessage + -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleConstructorError . P.constructors .~ cs + | (_cn, cs) <- Map.toList mulCtors + ] + if null mulFieldsErrs + then pure $ Sum ctors si + else throwError mulFieldsErrs toProto (Sum ctors si) = defMessage @@ -331,10 +362,18 @@ instance IsMessage P.Sum'Constructor Constructor where instance IsMessage P.Product'Record Record where fromProto r = do - fs' <- traverse fromProto $ r ^. P.fields + (fields, mulFields) <- collectMultipleKeys (\f -> f ^. #fieldName) (r ^. P.fields) si <- fromProto $ r ^. P.sourceInfo - fs <- maybe (throwProtoError $ EmptyRecordBody si) return $ nonEmpty fs' - pure $ Record fs si + let mulFieldsErrs = + [ ProtoParseError $ + defMessage + -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleFieldError . P.fields .~ fs + | (_fn, fs) <- Map.toList mulFields + ] + if null mulFieldsErrs + then pure $ Record fields si + else throwError mulFieldsErrs toProto (Record fs si) = defMessage @@ -354,7 +393,7 @@ instance IsMessage P.Product'NTuple Tuple where instance IsMessage P.Product Product where fromProto p = case p ^. P.maybe'product of - Nothing -> throwProtoError $ OneOfNotSet "product" + Nothing -> throwOneOfError (messageName (Proxy @P.Product)) "product" Just x -> case x of --- wrong, fix P.Product'Record' r -> do @@ -409,7 +448,7 @@ instance IsMessage P.TyClassRef'Foreign ForeignClassRef where instance IsMessage P.TyClassRef TyClassRef where fromProto tr = case tr ^. P.maybe'classRef of - Nothing -> throwProtoError $ OneOfNotSet "class_ref" + Nothing -> throwOneOfError (messageName (Proxy @P.TyClassRef)) "class_ref" Just x -> case x of P.TyClassRef'LocalClassRef lr -> LocalCI <$> fromProto lr P.TyClassRef'ForeignClassRef f -> ForeignCI <$> fromProto f @@ -426,7 +465,7 @@ instance IsMessage P.ClassDef ClassDef where carg <- case cargs of [] -> throwProtoError $ NoClassArgs cnm si [x] -> return x - _ -> throwProtoError $ MultipleClassArgs cnm si + _ -> throwInternalError "Multi parameter type classes are not supported" sups <- traverse fromProto $ cd ^. P.supers let doc = cd ^. P.documentation pure $ ClassDef cnm carg sups doc si @@ -448,7 +487,7 @@ instance IsMessage P.InstanceClause InstanceClause where hd <- case hds of [] -> throwProtoError $ NoInstanceHead cnm si [x] -> return x - xs -> throwProtoError $ MultipleInstanceHeads cnm xs si + _ -> throwInternalError "Multiple instance head, but multi parameter type classes are not supported" pure $ InstanceClause cnm hd csts si toProto (InstanceClause cnm hd csts si) = @@ -466,7 +505,7 @@ instance IsMessage P.Constraint Constraint where arg <- case args of [] -> throwProtoError $ NoConstraintArgs cnm si [x] -> return x - xs -> throwProtoError $ MultipleConstraintArgs cnm xs si + _ -> throwInternalError "Multiple instance constraint arguments, but multi parameter type classes are not supported" pure $ Constraint cnm arg si toProto (Constraint cnm arg si) = @@ -479,33 +518,70 @@ instance IsMessage P.Constraint Constraint where Module, CompilerInput -} +collectMultipleKeys :: forall {t :: Type -> Type} {proto} {a} {k}. (Foldable t, IsMessage proto a, Ord k) => (a -> k) -> t proto -> FromProto (Map k a, Map k [proto]) +collectMultipleKeys key = + foldlM + ( \(good, bad) px -> do + x <- fromProto px + if Map.member (key x) good + then return (good, Map.insertWith (++) (key x) [px] bad) + else return (Map.insert (key x) x good, bad) + ) + (mempty, mempty) + instance IsMessage P.Module Module where fromProto m = do mnm <- fromProto $ m ^. P.moduleName - tdefs <- traverse fromProto $ m ^. P.typeDefs - cdefs <- traverse fromProto $ m ^. P.classDefs + (tydefs, mulTyDefs) <- collectMultipleKeys (\tyDef -> tyDef ^. #tyName) (m ^. P.typeDefs) + (cldefs, mulClDefs) <- collectMultipleKeys (\cldef -> cldef ^. #className) (m ^. P.classDefs) + (impts, mulImpts) <- collectMultipleKeys (id @ModuleName) (m ^. P.imports) insts <- traverse fromProto $ m ^. P.instances - impts <- traverse fromProto $ m ^. P.imports si <- fromProto $ m ^. P.sourceInfo - pure $ Module mnm tdefs cdefs insts impts si + let mulTyDefsErrs = + [ ProtoParseError $ + defMessage + & P.multipleTydefError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleTydefError . P.tyDefs .~ tds + | (_tn, tds) <- Map.toList mulTyDefs + ] + mulClassDefsErrs = + [ ProtoParseError $ + defMessage + & P.multipleClassdefError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleClassdefError . P.classDefs .~ cds + | (_cn, cds) <- Map.toList mulClDefs + ] + protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs + if null protoParseErrs + then pure $ Module mnm tydefs cldefs insts (Map.keysSet impts) si + else throwError protoParseErrs toProto (Module mnm tdefs cdefs insts impts si) = defMessage & P.moduleName .~ toProto mnm - & P.typeDefs .~ (toProto <$> tdefs) - & P.classDefs .~ (toProto <$> cdefs) + & P.typeDefs .~ (toProto <$> toList tdefs) + & P.classDefs .~ (toProto <$> toList cdefs) & P.instances .~ (toProto <$> insts) - & P.imports .~ (toProto <$> impts) + & P.imports .~ (toProto <$> Set.toList impts) & P.sourceInfo .~ toProto si instance IsMessage P.CompilerInput CompilerInput where fromProto ci = do - ms <- traverse fromProto $ ci ^. P.modules - pure $ CompilerInput ms + (mods, mulModules) <- collectMultipleKeys (\m -> m ^. #moduleName) (ci ^. P.modules) + let mulModulesErrs = + [ ProtoParseError $ + defMessage + -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleModuleError . P.modules .~ ms + | (_mn, ms) <- Map.toList mulModules + ] + if null mulModulesErrs + then pure $ CompilerInput mods + else throwError mulModulesErrs toProto (CompilerInput ms) = defMessage - & P.modules .~ (toProto <$> ms) + & P.modules .~ (toProto <$> toList ms) {- Names @@ -583,33 +659,33 @@ instance IsMessage P.KindCheckError KindCheckError where & (P.inconsistentTypeError . P.inferredKind) .~ toProto ki & (P.inconsistentTypeError . P.definedKind) .~ toProto kd -instance IsMessage P.CompilerError CompilerError where - fromProto cErr = case cErr ^. P.maybe'compilerError of - Just x -> case x of - P.CompilerError'KindCheckError err -> CompKindCheckError <$> fromProto err - P.CompilerError'InternalError err -> InternalError <$> fromProto (err ^. P.internalError) - Nothing -> throwProtoError EmptyField - - toProto = \case - CompKindCheckError err -> defMessage & P.kindCheckError .~ toProto err - InternalError err -> defMessage & (P.internalError . P.internalError) .~ toProto err - -instance IsMessage P.CompilerResult CompilerResult where - fromProto c = - if c == defMessage - then pure CompilerResult - else throwProtoError EmptyField - toProto CompilerResult = defMessage - -instance IsMessage P.CompilerOutput CompilerOutput where - fromProto co = case co ^. P.maybe'compilerOutput of - Just (P.CompilerOutput'CompilationResult res) -> Right <$> fromProto res - Just (P.CompilerOutput'CompilationError err) -> Left <$> fromProto err - Nothing -> throwProtoError EmptyField - - toProto = \case - Right res -> defMessage & P.compilationResult .~ toProto res - Left err -> defMessage & P.compilationError .~ toProto err +-- instance IsMessage P.CompilerError CompilerError where +-- fromProto cErr = case cErr ^. P.maybe'compilerError of +-- Just x -> case x of +-- P.CompilerError'KindCheckError err -> CompKindCheckError <$> fromProto err +-- P.CompilerError'InternalError err -> InternalError <$> fromProto (err ^. P.internalError) +-- Nothing -> throwProtoError EmptyField + +-- toProto = \case +-- CompKindCheckError err -> defMessage & P.kindCheckError .~ toProto err +-- InternalError err -> defMessage & (P.internalError . P.internalError) .~ toProto err + +-- instance IsMessage P.CompilerResult CompilerResult where +-- fromProto c = +-- if c == defMessage +-- then pure CompilerResult +-- else throwProtoError EmptyField +-- toProto CompilerResult = defMessage + +-- instance IsMessage P.CompilerOutput CompilerOutput where +-- fromProto co = case co ^. P.maybe'compilerOutput of +-- Just (P.CompilerOutput'CompilerResult res) -> Right <$> fromProto res +-- Just (P.CompilerOutput'CompilerError err) -> Left <$> fromProto err +-- Nothing -> throwProtoError EmptyField + +-- toProto = \case +-- Right res -> defMessage & P.compilerResult .~ toProto res +-- Left err -> defMessage & P.compilerError .~ toProto err -- | Convert from internal Kind to Proto Kind. kind2ProtoKind :: K.Kind -> Kind diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 9a460833..4ecc5197 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -50,9 +50,9 @@ module LambdaBuffers.Compiler.ProtoCompat.Types ( module VARS, ) where --- for NonEmpty import Control.Exception (Exception) -import Data.List.NonEmpty (NonEmpty) +import Data.Map (Map) +import Data.Set (Set) import Data.Text (Text) import GHC.Generics (Generic) import LambdaBuffers.Compiler.KindCheck.Variable as VARS (Atom, Variable) @@ -145,7 +145,7 @@ instance Arbitrary Ty where , TyRefI <$> arbitrary ] -data TyApp = TyApp {tyFunc :: Ty, tyArgs :: NonEmpty Ty, sourceInfo :: SourceInfo} +data TyApp = TyApp {tyFunc :: Ty, tyArgs :: [Ty], sourceInfo :: SourceInfo} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary TyApp @@ -165,7 +165,7 @@ data TyDef = TyDef {tyName :: TyName, tyAbs :: TyAbs, sourceInfo :: SourceInfo} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary TyDef -data TyAbs = TyAbs {tyArgs :: [TyArg], tyBody :: TyBody, sourceInfo :: SourceInfo} +data TyAbs = TyAbs {tyArgs :: Map VarName TyArg, tyBody :: TyBody, sourceInfo :: SourceInfo} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary TyAbs @@ -181,7 +181,7 @@ data Constructor = Constructor {constrName :: ConstrName, product :: Product} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary Constructor -data Sum = Sum {constructors :: NonEmpty Constructor, sourceInfo :: SourceInfo} +data Sum = Sum {constructors :: Map ConstrName Constructor, sourceInfo :: SourceInfo} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary Sum @@ -189,7 +189,7 @@ data Field = Field {fieldName :: FieldName, fieldTy :: Ty} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary Field -data Record = Record {fields :: NonEmpty Field, sourceInfo :: SourceInfo} +data Record = Record {fields :: Map FieldName Field, sourceInfo :: SourceInfo} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary Record @@ -257,10 +257,10 @@ data Constraint = Constraint data Module = Module { moduleName :: ModuleName - , typeDefs :: [TyDef] - , classDefs :: [ClassDef] + , typeDefs :: Map TyName TyDef + , classDefs :: Map ClassName ClassDef , instances :: [InstanceClause] - , imports :: [ModuleName] + , imports :: Set ModuleName , sourceInfo :: SourceInfo } deriving stock (Show, Eq, Ord, Generic) @@ -295,7 +295,7 @@ data KindCheckErr instance Exception KindCheckErr -newtype CompilerInput = CompilerInput {modules :: [Module]} +newtype CompilerInput = CompilerInput {modules :: Map ModuleName Module} deriving stock (Show, Eq, Ord, Generic) deriving newtype (Monoid, Semigroup) diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index ed9f9173..ddd61979 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -1,14 +1,13 @@ module Test.KindCheck (test) where import Data.Bifunctor (Bifunctor (bimap)) -import Data.List.NonEmpty (NonEmpty ((:|)), cons) import Data.Text (Text) import LambdaBuffers.Compiler.KindCheck ( check_, foldWithProduct, foldWithSum, ) -import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var)) +import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var), tyEither, tyProd, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable ( Variable (LocalRef), ) @@ -32,7 +31,7 @@ import Test.Utils.CompilerInput ( compilerInput'incoherent, compilerInput'maybe, ) -import Test.Utils.Constructors (_ModuleName) +import Test.Utils.Constructors (_CompilerInput, _ModuleName) import Test.Utils.TyDef (tyDef'maybe) -------------------------------------------------------------------------------- @@ -69,7 +68,7 @@ testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe, kcTestFai trivialKCTest :: TestTree trivialKCTest = testCase "Empty CompInput should check." $ - check_ (P.CompilerInput []) @?= Right () + check_ (_CompilerInput []) @?= Right () kcTestMaybe :: TestTree kcTestMaybe = @@ -98,7 +97,7 @@ kcTestOrdering = genModuleIn2Layouts = do mods <- arbitrary shuffledMods <- shuffle mods - pure (P.CompilerInput mods, P.CompilerInput shuffledMods) + pure (_CompilerInput mods, _CompilerInput shuffledMods) eitherFailOrPass :: forall {a} {c}. Either a c -> Either () () eitherFailOrPass = bimap (const ()) (const ()) @@ -114,27 +113,31 @@ testFolds = , testGroup "Test Sum Folds." [testSumFold1, testSumFold2, testSumFold3] ] --- | [ a ] -> a +prod :: Type -> Type -> Type +prod = App . App (Var tyProd) + +unit' :: Type +unit' = Var tyUnit + +-- | [ a ] -> prod unit a testFoldProd1 :: TestTree testFoldProd1 = testCase "Fold with product - 1 type." $ - foldWithProduct (lVar "a" :| []) @?= lVar "a" + foldWithProduct [lVar "a"] @?= prod unit' (lVar "a") --- | [a ,b] -> (a,b) +-- | [b ,a] -> prod (prod unit b) a testFoldProd2 :: TestTree testFoldProd2 = testCase "Fold with product - 2 types." $ - foldWithProduct (cons (lVar "b") $ lVar "a" :| []) - @?= App (App (lVar "Π") (lVar "b")) (lVar "a") + foldWithProduct [lVar "b", lVar "a"] + @?= prod (prod unit' (lVar "b")) (lVar "a") --- | [ a, b ,c ] -> (a,(b,c)) +-- | [ a, b ,c ] -> prod (prod (prod unit c) b) a testFoldProd3 :: TestTree testFoldProd3 = testCase "Fold with product - 2 types." $ - foldWithProduct (cons (lVar "c") $ cons (lVar "b") $ lVar "a" :| []) - @?= App - (App (lVar "Π") (lVar "c")) - (App (App (lVar "Π") (lVar "b")) (lVar "a")) + foldWithProduct [lVar "c", lVar "b", lVar "a"] + @?= prod (prod (prod unit' (lVar "c")) (lVar "b")) (lVar "a") testPProdFoldTotal :: TestTree testPProdFoldTotal = @@ -142,27 +145,31 @@ testPProdFoldTotal = forAll arbitrary $ \ts -> foldWithProduct ts === foldWithProduct ts --- | [ a ] -> a +either' :: Type -> Type -> Type +either' = App . App (Var tyEither) + +void' :: Type +void' = Var tyVoid + +-- | [ a ] -> either void a testSumFold1 :: TestTree testSumFold1 = testCase "Fold 1 type." $ - foldWithSum (lVar "a" :| []) @?= lVar "a" + foldWithSum [lVar "a"] @?= either' void' (lVar "a") --- | [ a , b ] -> a | b +-- | [ a , b ] -> either (either void a) b testSumFold2 :: TestTree testSumFold2 = testCase "Fold 2 type." $ - foldWithSum (cons (lVar "b") $ lVar "a" :| []) - @?= App (App (lVar "Σ") (lVar "b")) (lVar "a") + foldWithSum [lVar "b", lVar "a"] + @?= either' (either' void' (lVar "b")) (lVar "a") -- | [ a , b , c ] -> a | ( b | c ) testSumFold3 :: TestTree testSumFold3 = testCase "Fold 3 types." $ - foldWithSum (cons (lVar "c") $ cons (lVar "b") $ lVar "a" :| []) - @?= App - (App (lVar "Σ") (lVar "c")) - (App (App (lVar "Σ") (lVar "b")) (lVar "a")) + foldWithSum [lVar "c", lVar "b", lVar "a"] + @?= either' (either' (either' void' (lVar "c")) (lVar "b")) (lVar "a") -- | TyDef to Kind Canonical representation - sums not folded - therefore we get constructor granularity. Might use in a different implementation for more granular errors. lVar :: Text -> Type diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index 910c7291..6c60fd7a 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -1,20 +1,18 @@ module Test.Utils.CompilerInput (compilerInput'incoherent, compilerInput'maybe, compilerInput'doubleDeclarationDiffMod, compilerInput'doubleDeclaration) where -import Control.Lens ((%~), (&), (.~)) +import Control.Lens ((%~), (&)) import LambdaBuffers.Compiler.ProtoCompat qualified as P +import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module (module'incoherent, module'maybe) import Test.Utils.SourceInfo (sourceInfo'empty) -_CompilerInput :: [P.Module] -> P.CompilerInput -_CompilerInput x = P.CompilerInput {P.modules = x} - -- | Compiler Input containing 1 module with 1 definition - Maybe. compilerInput'maybe :: P.CompilerInput compilerInput'maybe = _CompilerInput [module'maybe] -- | Contains 2 definitions - 1 wrong one. compilerInput'incoherent :: P.CompilerInput -compilerInput'incoherent = compilerInput'maybe & #modules .~ [module'incoherent] +compilerInput'incoherent = _CompilerInput [module'maybe, module'incoherent] -- | Declares maybe twice. compilerInput'doubleDeclaration :: P.CompilerInput diff --git a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs index ee15385e..12101c2c 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs @@ -13,21 +13,29 @@ module Test.Utils.Constructors ( _TyDef, _TyRefILocal, _Module, + _CompilerInput, _ModuleName, _ModuleNamePart, ) where -import Data.List.NonEmpty (fromList) +import Control.Lens ((^.)) +import Data.Map qualified as Map import Data.Text (Text) import LambdaBuffers.Compiler.ProtoCompat qualified as P import Test.Utils.SourceInfo (sourceInfo'empty) +_CompilerInput :: [P.Module] -> P.CompilerInput +_CompilerInput ms = + P.CompilerInput + { P.modules = Map.fromList [(m ^. #moduleName, m) | m <- ms] + } + _Module :: P.ModuleName -> [P.TyDef] -> [P.ClassDef] -> [P.InstanceClause] -> P.Module _Module mn tds cds ins = P.Module { P.moduleName = mn - , P.typeDefs = tds - , P.classDefs = cds + , P.typeDefs = Map.fromList [(td ^. #tyName, td) | td <- tds] + , P.classDefs = Map.fromList [(cd ^. #className, cd) | cd <- cds] , P.instances = ins , P.imports = mempty , P.sourceInfo = sourceInfo'empty @@ -81,14 +89,14 @@ _Sum :: [(Text, P.Product)] -> P.TyBody _Sum cs = P.SumI $ P.Sum - { constructors = fromList $ uncurry _Constructor <$> cs + { constructors = Map.fromList [(ctor ^. #constrName, ctor) | (cn, cp) <- cs, ctor <- [_Constructor cn cp]] , sourceInfo = sourceInfo'empty } _TyAbs :: [(Text, P.KindType)] -> [(Text, P.Product)] -> P.TyAbs _TyAbs args body = P.TyAbs - { P.tyArgs = _TyArg <$> args + { P.tyArgs = Map.fromList [(ta ^. #argName, ta) | ta <- _TyArg <$> args] , P.tyBody = _Sum body , sourceInfo = sourceInfo'empty } diff --git a/lambda-buffers-compiler/test/Test/Utils/Module.hs b/lambda-buffers-compiler/test/Test/Utils/Module.hs index 02148b8f..73963406 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Module.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Module.hs @@ -1,24 +1,13 @@ module Test.Utils.Module (module'maybe, module'incoherent) where -import Control.Lens ((%~), (&)) import LambdaBuffers.Compiler.ProtoCompat qualified as P -import Test.Utils.SourceInfo (sourceInfo'empty) +import Test.Utils.Constructors (_Module, _ModuleName) import Test.Utils.TyDef (tyDef'incoherent, tyDef'maybe) +-- _Module mn tds cds ins = + module'maybe :: P.Module -module'maybe = - P.Module - { P.moduleName = - P.ModuleName - { P.parts = [P.ModuleNamePart "Module" sourceInfo'empty] - , P.sourceInfo = sourceInfo'empty - } - , P.typeDefs = [tyDef'maybe] - , P.classDefs = mempty - , P.instances = mempty - , P.sourceInfo = sourceInfo'empty - , P.imports = mempty - } +module'maybe = _Module (_ModuleName ["Module"]) [tyDef'maybe] mempty mempty {- | 1 Module containing Maybe = ... @@ -30,4 +19,4 @@ module'maybe = Type -> Type. This is an inconsistency failure. -} module'incoherent :: P.Module -module'incoherent = module'maybe & #typeDefs %~ (<> [tyDef'incoherent]) +module'incoherent = _Module (_ModuleName ["Module"]) [tyDef'maybe, tyDef'incoherent] mempty mempty diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index afdb340c..d1b8bc13 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -189,23 +189,6 @@ message ClassName { SourceInfo source_info = 2; } -/* Naming error message */ -message NamingError { - enum NameType { - NAME_TYPE_UNSPECIFIED = 0; - NAME_TYPE_MODULE = 1; - NAME_TYPE_TYPE = 2; - NAME_TYPE_VAR = 3; - NAME_TYPE_CONSTR = 4; - NAME_TYPE_FIELD = 5; - NAME_TYPE_CLASS = 6; - }; - // Type of name. - NameType name_type = 1; - // Source information. - SourceInfo source_info = 2; -} - /* Type definition A type definition consists of a type name and its associated type term. @@ -526,50 +509,88 @@ message CompilerInput { // Internal errors. message InternalError { - string internal_error = 1; -} + string msg = 1; +} + +// All errors that occur because of Google Protocol Buffer's inability to +// enforce certain invariants. +// Some of invariance: +// - using Proto `map` restricts users to `string` keys which impacts +// API documentation, which is why `repeated` fields are used throughout, +// - using Proto 'oneof' means users have to check if such a field is +// set or report an error otherwise. +message ProtoParseError { + // Multiple Modules with the same ModuleName were found. + message MultipleModuleError { + // Conflicting type definitions. + repeated Module modules = 2; + } -// Multiple Modules with the same ModuleName were found. -message MultipleModuleError { - // Conflicting type definitions. - repeated Module modules = 2; -} + // Multiple TyDefs with the same TyName were found in ModuleName. + message MultipleTyDefError { + // Module in which the error was found. + ModuleName module_name = 1; + // Conflicting type definitions. + repeated TyDef ty_defs = 2; + } -// Multiple TyDefs with the same TyName were found in ModuleName. -message MultipleTyDefError { - // Module in which the error was found. - ModuleName module_name = 1; - // Conflicting type definitions. - repeated TyDef ty_defs = 2; -} + // Multiple ClassDefs with the same ClassName were found in ModuleName. + message MultipleClassDefError { + // Module in which the error was found. + ModuleName module_name = 1; + // Conflicting class definitions. + repeated ClassDef class_defs = 2; + } -// Multiple ClassDefs with the same ClassName were found in ModuleName. -message MultipleClassDefError { - // Module in which the error was found. - ModuleName module_name = 1; - // Conflicting class definitions. - repeated ClassDef class_defs = 2; -} + // Multiple TyArgs with the same ArgName were found in ModuleName.TyDef. + message MultipleTyArgError { + // Module in which the error was found. + ModuleName module_name = 1; + // Type definition in which the error was found. + TyDef ty_def = 2; + // Conflicting type abstraction arguments. + repeated TyArg ty_args = 3; + } -// Multiple TyArgs with the same ArgName were found in ModuleName.TyDef. -message MultipleTyArgError { - // Module in which the error was found. - ModuleName module_name = 1; - // Type definition in which the error was found. - TyDef ty_def = 2; - // Conflicting type abstraction arguments. - repeated TyArg ty_args = 3; -} + // Multiple Sum Constructors with the same ConstrName were found in + // ModuleName.TyDef. + message MultipleConstructorError { + // Module in which the error was found. + ModuleName module_name = 1; + // Type definition in which the error was found. + TyDef ty_def = 2; + // Conflicting constructors. + repeated Sum.Constructor constructors = 3; + } -// Multiple Sum Constructors with the same ConstrName were found in -// ModuleName.TyDef. -message MultipleConstructorError { - // Module in which the error was found. - ModuleName module_name = 1; - // Type definition in which the error was found. - TyDef ty_def = 2; - // Conflicting constructors. - repeated Sum.Constructor constructors = 3; + // Multiple Record Fields with the same FieldName were found in + // ModuleName.TyDef. + message MultipleFieldError { + // Module in which the error was found. + ModuleName module_name = 1; + // Type definition in which the error was found. + TyDef ty_def = 2; + // Conflicting record fields. + repeated Product.Record.Field fields = 3; + } + + // Proto `oneof` field is not set. + message OneOfNotSetError { + // Proto message name in which the `oneof` field is not set. + string message_name = 1; + // The `oneof` field that is not set. + string field_name = 2; + } + + oneof proto_parse_error { + MultipleModuleError multiple_module_error = 1; + MultipleTyDefError multiple_tydef_error = 2; + MultipleClassDefError multiple_classdef_error = 3; + MultipleTyArgError multiple_tyarg_error = 4; + MultipleConstructorError multiple_constructor_error = 5; + MultipleFieldError multiple_field_error = 6; + OneOfNotSetError one_of_not_set_error = 7; + } } // Kind checking errors. @@ -596,7 +617,6 @@ message KindCheckError { Kind ty_kind_2 = 3; } - // Error reads: // Inifinitely recursive term detected in definition ty_name. message RecursiveKindError { TyName ty_name = 1; @@ -609,7 +629,7 @@ message KindCheckError { Kind defined_kind = 3; } - // The types of inference errors. + // One of the errors occurred during kind checking. oneof kind_check_error { UnboundTermError unbound_term_error = 1; ImpossibleUnificationError unification_error = 2; @@ -618,30 +638,39 @@ message KindCheckError { } } -// Compiler Error can be extended with other classes of errors. -message CompilerError { - - // Reason why the compilation failed. - oneof compiler_error { - MultipleModuleError multiple_module_error = 1; - MultipleTyDefError multiple_tydef_error = 2; - MultipleClassDefError multiple_classdef_error = 3; - MultipleTyArgError multiple_tyarg_error = 4; - MultipleConstructorError multiple_constructor_error = 5; - KindCheckError kind_check_error = 6; - InternalError internal_error = 7; +/* Naming error message */ +message NamingError { + // One of naming errors. + oneof naming_error { + ModuleNamePart module_name_err = 1; + TyName ty_name_err = 2; + VarName var_name_err = 3; + ConstrName constr_name_err = 4; + FieldName field_name_err = 5; + ClassName class_name_err = 6; } } +// Compiler Error +message CompilerError { + // Errors occurred during a proto parsing. + repeated ProtoParseError proto_parse_errors = 1; + // Errors occurred during naming checking. + repeated NamingError naming_errors = 2; + // Errors occurred during kind checking. + repeated KindCheckError kind_check_errors = 4; + // Errors internal to the compiler implementation. + repeated InternalError internal_errors = 5; +} + // Compiler Result ~ a successful Compilation Output. message CompilerResult { - // equivalent of unit. } // Output of the Compiler. message CompilerOutput { oneof compiler_output { - CompilerError compilation_error = 1; - CompilerResult compilation_result = 2; + CompilerError compiler_error = 1; + CompilerResult compiler_result = 2; } } From fc223016143b9331466ecd3009ed0d847a112410 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Mon, 13 Feb 2023 19:37:20 +0100 Subject: [PATCH 06/20] Added tests for empty folds --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 4 ++-- lambda-buffers-compiler/test/Test/KindCheck.hs | 16 ++++++++++++++-- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index bc48f8d3..58b8fcbd 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -125,8 +125,8 @@ localStrategy :: Transform ModuleCheck KindCheck localStrategy = reinterpret $ \case KCTypeDefinition mname ctx tydef -> do kindFromTyDef mname tydef >>= inferTypeKind mname tydef ctx >>= checkKindConsistency mname tydef ctx - KCClassInstance _ctx _instClause -> pure () -- "FIXME(cstml)" - KCClass _ctx _classDef -> pure () -- "FIXME(cstml)" + KCClassInstance _ctx _instClause -> pure () -- FIXME(cstml) + KCClass _ctx _classDef -> pure () -- FIXME(cstml) runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a runKindCheck = interpret $ \case diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index ddd61979..5fa1d536 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -109,8 +109,8 @@ testFolds :: TestTree testFolds = testGroup "Test Folds" - [ testGroup "Test Product Folds." [testFoldProd1, testFoldProd2, testFoldProd3, testPProdFoldTotal] - , testGroup "Test Sum Folds." [testSumFold1, testSumFold2, testSumFold3] + [ testGroup "Test Product Folds." [testFoldProd0, testFoldProd1, testFoldProd2, testFoldProd3, testPProdFoldTotal] + , testGroup "Test Sum Folds." [testSumFold0, testSumFold1, testSumFold2, testSumFold3] ] prod :: Type -> Type -> Type @@ -119,6 +119,12 @@ prod = App . App (Var tyProd) unit' :: Type unit' = Var tyUnit +-- | [ ] -> unit +testFoldProd0 :: TestTree +testFoldProd0 = + testCase "Fold with product - 0 type." $ + foldWithProduct [] @?= unit' + -- | [ a ] -> prod unit a testFoldProd1 :: TestTree testFoldProd1 = @@ -151,6 +157,12 @@ either' = App . App (Var tyEither) void' :: Type void' = Var tyVoid +-- | [ ] -> void +testSumFold0 :: TestTree +testSumFold0 = + testCase "Fold 0 type." $ + foldWithSum [] @?= void' + -- | [ a ] -> either void a testSumFold1 :: TestTree testSumFold1 = From e66b83375e61e1468111ad0bfe7093ba06c47a03 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Mon, 13 Feb 2023 20:25:37 +0100 Subject: [PATCH 07/20] Purging the mul ty def from KindCheck modules and tests --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 10 ++---- .../src/LambdaBuffers/Compiler/ProtoCompat.hs | 35 +++++++++++-------- .../Compiler/ProtoCompat/Types.hs | 1 - .../test/Test/KindCheck.hs | 27 ++------------ .../test/Test/Utils/CompilerInput.hs | 16 +-------- lambda-buffers-proto/compiler.proto | 21 +++++++++-- 6 files changed, 45 insertions(+), 65 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 58b8fcbd..c2546819 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -16,7 +16,7 @@ import Control.Monad (void) import Control.Monad.Freer (Eff, Member, Members, interpret, reinterpret, run) import Control.Monad.Freer.Error (Error, runError, throwError) import Control.Monad.Freer.Reader (Reader, ask, runReader) -import Control.Monad.Freer.State (State, evalState, get, modify) +import Control.Monad.Freer.State (State, evalState, modify) import Control.Monad.Freer.TH (makeEffect) import Data.Foldable (Foldable (foldl', toList), traverse_) import Data.Map qualified as M @@ -225,13 +225,7 @@ tyDef2Context curModName tyDef = do -- Ads the name to our map - we can use its SourceLocation in the case of a -- double use. If it's already in our map - that means we've double declared it. associateName :: Variable -> P.TyDef -> Eff effs () - associateName v curTyDef = do - modName <- ask - maps <- get @(M.Map Variable P.TyDef) - case maps M.!? v of - Just otherTyDef -> - throwError . PT.CompKindCheckError $ PT.MultipleTyDefError modName [otherTyDef, curTyDef] - Nothing -> modify (M.insert v curTyDef) + associateName v curTyDef = modify (M.insert v curTyDef) {- | Converts the Proto Module name to a local modname - dropping the information. diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs index b36ed9d8..77f196b2 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs @@ -255,7 +255,7 @@ instance IsMessage P.TyDef TyDef where instance IsMessage P.TyAbs TyAbs where fromProto ta = do - (tyargs, mulTyArgs) <- collectMultipleKeys (\a -> a ^. #argName) (ta ^. P.tyArgs) + (tyargs, mulTyArgs) <- parseAndIndex (\a -> a ^. #argName) (ta ^. P.tyArgs) tybody <- fromProto $ ta ^. P.tyBody si <- fromProto $ ta ^. P.sourceInfo let mulArgsErrs = @@ -330,7 +330,7 @@ instance IsMessage P.TyBody TyBody where instance IsMessage P.Sum Sum where fromProto s = do - (ctors, mulCtors) <- collectMultipleKeys (\c -> c ^. #constrName) (s ^. P.constructors) + (ctors, mulCtors) <- parseAndIndex (\c -> c ^. #constrName) (s ^. P.constructors) si <- fromProto $ s ^. P.sourceInfo -- TODO(bladyjoker): ctors <- maybe (throwProtoError $ EmptySumBody si) return $ nonEmpty ctors' let mulFieldsErrs = @@ -362,7 +362,7 @@ instance IsMessage P.Sum'Constructor Constructor where instance IsMessage P.Product'Record Record where fromProto r = do - (fields, mulFields) <- collectMultipleKeys (\f -> f ^. #fieldName) (r ^. P.fields) + (fields, mulFields) <- parseAndIndex (\f -> f ^. #fieldName) (r ^. P.fields) si <- fromProto $ r ^. P.sourceInfo let mulFieldsErrs = [ ProtoParseError $ @@ -518,23 +518,23 @@ instance IsMessage P.Constraint Constraint where Module, CompilerInput -} -collectMultipleKeys :: forall {t :: Type -> Type} {proto} {a} {k}. (Foldable t, IsMessage proto a, Ord k) => (a -> k) -> t proto -> FromProto (Map k a, Map k [proto]) -collectMultipleKeys key = +parseAndIndex :: forall {t :: Type -> Type} {proto} {a} {k}. (Foldable t, IsMessage proto a, Ord k) => (a -> k) -> t proto -> FromProto (Map k a, Map k [proto]) +parseAndIndex key = foldlM - ( \(good, bad) px -> do + ( \(indexed, multiples) px -> do x <- fromProto px - if Map.member (key x) good - then return (good, Map.insertWith (++) (key x) [px] bad) - else return (Map.insert (key x) x good, bad) + if Map.member (key x) indexed + then return (indexed, Map.insertWith (++) (key x) [px] multiples) + else return (Map.insert (key x) x indexed, multiples) ) (mempty, mempty) instance IsMessage P.Module Module where fromProto m = do mnm <- fromProto $ m ^. P.moduleName - (tydefs, mulTyDefs) <- collectMultipleKeys (\tyDef -> tyDef ^. #tyName) (m ^. P.typeDefs) - (cldefs, mulClDefs) <- collectMultipleKeys (\cldef -> cldef ^. #className) (m ^. P.classDefs) - (impts, mulImpts) <- collectMultipleKeys (id @ModuleName) (m ^. P.imports) + (tydefs, mulTyDefs) <- parseAndIndex (\tyDef -> tyDef ^. #tyName) (m ^. P.typeDefs) + (cldefs, mulClDefs) <- parseAndIndex (\cldef -> cldef ^. #className) (m ^. P.classDefs) + (impts, mulImpts) <- parseAndIndex (\(mn :: ModuleName) -> mn) (m ^. P.imports) insts <- traverse fromProto $ m ^. P.instances si <- fromProto $ m ^. P.sourceInfo let mulTyDefsErrs = @@ -551,7 +551,14 @@ instance IsMessage P.Module Module where & P.multipleClassdefError . P.classDefs .~ cds | (_cn, cds) <- Map.toList mulClDefs ] - protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs + mulImptsErrs = + [ ProtoParseError $ + defMessage + & P.multipleImportError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleImportError . P.imports .~ ims + | (_in, ims) <- Map.toList mulImpts + ] + protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs ++ mulImptsErrs if null protoParseErrs then pure $ Module mnm tydefs cldefs insts (Map.keysSet impts) si else throwError protoParseErrs @@ -567,7 +574,7 @@ instance IsMessage P.Module Module where instance IsMessage P.CompilerInput CompilerInput where fromProto ci = do - (mods, mulModules) <- collectMultipleKeys (\m -> m ^. #moduleName) (ci ^. P.modules) + (mods, mulModules) <- parseAndIndex (\m -> m ^. #moduleName) (ci ^. P.modules) let mulModulesErrs = [ ProtoParseError $ defMessage diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 4ecc5197..eea25264 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -309,7 +309,6 @@ data KindCheckError | IncorrectApplicationError TyName Kind Kind | RecursiveKindError TyName | InconsistentTypeError TyName Kind Kind - | MultipleTyDefError ModuleName [TyDef] deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary KindCheckError instance Exception KindCheckError diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index 5fa1d536..b4374912 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -11,7 +11,6 @@ import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var), tyEither, tyProd, import LambdaBuffers.Compiler.KindCheck.Variable ( Variable (LocalRef), ) -import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P import Test.QuickCheck ( Arbitrary (arbitrary, shrink), @@ -26,38 +25,16 @@ import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertBool, testCase, (@?=)) import Test.Tasty.QuickCheck (testProperty) import Test.Utils.CompilerInput ( - compilerInput'doubleDeclaration, - compilerInput'doubleDeclarationDiffMod, compilerInput'incoherent, compilerInput'maybe, ) -import Test.Utils.Constructors (_CompilerInput, _ModuleName) -import Test.Utils.TyDef (tyDef'maybe) +import Test.Utils.Constructors (_CompilerInput) -------------------------------------------------------------------------------- -- Top Level tests test :: TestTree -test = testGroup "Compiler tests" [testCheck, testFolds, testRefl, testMultipleDec] - --------------------------------------------------------------------------------- --- Multiple declaration test - -testMultipleDec :: TestTree -testMultipleDec = testGroup "Multiple declaration tests." [doubleDeclaration, passingDoubleDeclaration] - -doubleDeclaration :: TestTree -doubleDeclaration = - testCase "Two declarations of Maybe within the same module are caught." $ - check_ compilerInput'doubleDeclaration - @?= Left (P.CompKindCheckError (P.MultipleTyDefError moduleName [tyDef'maybe, tyDef'maybe])) - where - moduleName = _ModuleName ["Module"] - -passingDoubleDeclaration :: TestTree -passingDoubleDeclaration = - testCase "Two declarations of Maybe within different modules are fine." $ - check_ compilerInput'doubleDeclarationDiffMod @?= Right () +test = testGroup "Compiler tests" [testCheck, testFolds, testRefl] -------------------------------------------------------------------------------- -- Module tests diff --git a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs index 6c60fd7a..859b44f6 100644 --- a/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs +++ b/lambda-buffers-compiler/test/Test/Utils/CompilerInput.hs @@ -1,10 +1,8 @@ -module Test.Utils.CompilerInput (compilerInput'incoherent, compilerInput'maybe, compilerInput'doubleDeclarationDiffMod, compilerInput'doubleDeclaration) where +module Test.Utils.CompilerInput (compilerInput'incoherent, compilerInput'maybe) where -import Control.Lens ((%~), (&)) import LambdaBuffers.Compiler.ProtoCompat qualified as P import Test.Utils.Constructors (_CompilerInput) import Test.Utils.Module (module'incoherent, module'maybe) -import Test.Utils.SourceInfo (sourceInfo'empty) -- | Compiler Input containing 1 module with 1 definition - Maybe. compilerInput'maybe :: P.CompilerInput @@ -13,15 +11,3 @@ compilerInput'maybe = _CompilerInput [module'maybe] -- | Contains 2 definitions - 1 wrong one. compilerInput'incoherent :: P.CompilerInput compilerInput'incoherent = _CompilerInput [module'maybe, module'incoherent] - --- | Declares maybe twice. -compilerInput'doubleDeclaration :: P.CompilerInput -compilerInput'doubleDeclaration = compilerInput'maybe <> compilerInput'maybe - --- | Declares maybe twice - in different modules -compilerInput'doubleDeclarationDiffMod :: P.CompilerInput -compilerInput'doubleDeclarationDiffMod = - compilerInput'maybe - <> _CompilerInput - [ module'maybe & #moduleName . #parts %~ (P.ModuleNamePart "Module" sourceInfo'empty :) - ] diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index d1b8bc13..7aad5932 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -574,6 +574,13 @@ message ProtoParseError { repeated Product.Record.Field fields = 3; } + message MultipleImportError { + // Module in which the error was found. + ModuleName module_name = 1; + // Conflicting module imports. + repeated ModuleName imports = 2; + } + // Proto `oneof` field is not set. message OneOfNotSetError { // Proto message name in which the `oneof` field is not set. @@ -582,6 +589,14 @@ message ProtoParseError { string field_name = 2; } + // Proto `enum` field is unknown. + message UnknownEnumError { + // Proto message name in which the `enum` field is unknown. + string message_name = 1; + // The `enum` field that is unknown. + string field_name = 2; + } + oneof proto_parse_error { MultipleModuleError multiple_module_error = 1; MultipleTyDefError multiple_tydef_error = 2; @@ -589,7 +604,9 @@ message ProtoParseError { MultipleTyArgError multiple_tyarg_error = 4; MultipleConstructorError multiple_constructor_error = 5; MultipleFieldError multiple_field_error = 6; - OneOfNotSetError one_of_not_set_error = 7; + MultipleImportError multiple_import_error = 7; + OneOfNotSetError one_of_not_set_error = 8; + UnknownEnumError unknown_enum_error = 9; } } @@ -653,7 +670,7 @@ message NamingError { // Compiler Error message CompilerError { - // Errors occurred during a proto parsing. + // Errors occurred during proto parsing. repeated ProtoParseError proto_parse_errors = 1; // Errors occurred during naming checking. repeated NamingError naming_errors = 2; From 3f57029519221466b1dfcc571f99b983dbc0d3d4 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 12:08:40 +0100 Subject: [PATCH 08/20] All errors are in the API now --- .../lambda-buffers-compiler.cabal | 1 - .../src/LambdaBuffers/Compiler/NamingCheck.hs | 14 +- .../src/LambdaBuffers/Compiler/ProtoCompat.hs | 319 ++++++++++-------- .../Compiler/ProtoCompat/Types.hs | 4 + .../test/Test/TypeClassCheck.hs | 66 ++-- .../test/Test/Utils/Constructors.hs | 33 +- .../test/Test/Utils/SourceInfo.hs | 7 - lambda-buffers-proto/compiler.proto | 17 +- 8 files changed, 254 insertions(+), 207 deletions(-) delete mode 100644 lambda-buffers-compiler/test/Test/Utils/SourceInfo.hs diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index 0add5645..3980a239 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -164,5 +164,4 @@ test-suite tests Test.Utils.CompilerInput Test.Utils.Constructors Test.Utils.Module - Test.Utils.SourceInfo Test.Utils.TyDef diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs index 3a7338c5..57d97cff 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/NamingCheck.hs @@ -1,16 +1,15 @@ -module LambdaBuffers.Compiler.NamingCheck (pModuleNamePart, pVarName, pTyName, pConstrName, pFieldName, pClassName, checkModuleName, checkTyName, checkVarName, checkConstrName, checkClassName, checkFieldName) where +module LambdaBuffers.Compiler.NamingCheck (pModuleNamePart, pVarName, pTyName, pConstrName, pFieldName, pClassName, checkModuleNamePart, checkTyName, checkVarName, checkConstrName, checkClassName, checkFieldName) where import Control.Lens (ASetter, (.~), (^.)) import Control.Monad.Except (MonadError (throwError)) -import Data.Foldable (for_) import Data.Function ((&)) import Data.Kind (Type) import Data.ProtoLens (Message (defMessage)) import Data.ProtoLens.Field (HasField) import Data.String (IsString (fromString)) import Data.Text (Text) -import Proto.Compiler (ClassName, ConstrName, FieldName, Module, NamingError, TyName, VarName) -import Proto.Compiler_Fields (classNameErr, constrNameErr, fieldNameErr, moduleName, moduleNameErr, name, parts, tyNameErr, varNameErr) +import Proto.Compiler (ClassName, ConstrName, FieldName, ModuleNamePart, NamingError, TyName, VarName) +import Proto.Compiler_Fields (classNameErr, constrNameErr, fieldNameErr, moduleNameErr, name, tyNameErr, varNameErr) import Text.Parsec (ParsecT, Stream, alphaNum, label, lower, many, many1, runParserT) import Text.Parsec.Char (upper) @@ -56,11 +55,8 @@ validateP p f i = do Left _ -> throwError $ defMessage & f .~ i Right _ -> return () -checkModuleName :: MonadError NamingError m => Module -> m () -checkModuleName m = - for_ - (m ^. (moduleName . parts)) - (validateP pModuleNamePart moduleNameErr) +checkModuleNamePart :: MonadError NamingError m => ModuleNamePart -> m () +checkModuleNamePart = validateP pModuleNamePart moduleNameErr checkTyName :: MonadError NamingError m => TyName -> m () checkTyName = validateP pTyName tyNameErr diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs index 77f196b2..60bfdcf6 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs @@ -4,66 +4,63 @@ module LambdaBuffers.Compiler.ProtoCompat ( IsMessage (..), FromProtoErr (..), - ProtoError (..), module X, protoKind2Kind, kind2ProtoKind, + runFromProto, ) where -- NOTE(cstml): I'm re-exporting the module from here as it makes more sense - -- also avoids annoying errors. import LambdaBuffers.Compiler.ProtoCompat.Types as X hiding (InternalError) -import Control.Lens (Getter, to, (&), (.~), (^.)) -import Control.Monad.Except (MonadError (throwError)) +import Control.Lens ((&), (.~), (^.)) +import Control.Monad.Except (Except, MonadError (throwError), runExcept) +import Control.Monad.Reader (MonadReader (ask, local), ReaderT (runReaderT)) import Data.Foldable (foldlM, toList) import Data.Generics.Labels () +import Data.Generics.Product (HasField) import Data.Kind (Type) import Data.Map (Map) import Data.Map qualified as Map -import Data.ProtoLens (Message (messageName), defMessage) +import Data.ProtoLens (Message (messageName), MessageEnum (showEnum), defMessage) import Data.Proxy (Proxy (Proxy)) import Data.Set qualified as Set import Data.Text (Text) import Data.Text qualified as Text import GHC.Generics (Generic) import LambdaBuffers.Compiler.KindCheck.Kind qualified as K -import LambdaBuffers.Compiler.NamingCheck (checkClassName, checkConstrName, checkFieldName, checkTyName, checkVarName) +import LambdaBuffers.Compiler.NamingCheck (checkClassName, checkConstrName, checkFieldName, checkModuleNamePart, checkTyName, checkVarName) import Proto.Compiler (NamingError) import Proto.Compiler qualified as P import Proto.Compiler_Fields qualified as P --- FIXME(bladyjoker): This emits a missing Functor constraint @gnumonik --- something like this probably exists in lens but i can't find it -traversing :: (Traversable t, Applicative f) => (a -> f b) -> Getter (t a) (f (t b)) -traversing f = to $ \ta -> traverse f ta - data FromProtoErr - = ProtoError ProtoError - | NamingError P.NamingError + = NamingError P.NamingError | InternalError P.InternalError | ProtoParseError P.ProtoParseError deriving stock (Show, Eq, Ord, Generic) -type FromProto a = forall m. MonadError [FromProtoErr] m => m a +data FromProtoContext + = CtxCompilerInput + | CtxModule P.ModuleName + | CtxTyDef P.ModuleName P.TyDef + | CtxClassDef P.ModuleName P.ClassDef + deriving stock (Show, Eq, Ord, Generic) + +type FromProto a = ReaderT FromProtoContext (Except [FromProtoErr]) a + +-- | Parse a Proto API CompilerInput into the internal CompilerInput representation or report errors. +runFromProto :: P.CompilerInput -> Either [FromProtoErr] CompilerInput +runFromProto compInp = do + let exM = runReaderT (fromProto compInp) CtxCompilerInput + runExcept exM class IsMessage (proto :: Type) (good :: Type) where fromProto :: proto -> FromProto good toProto :: good -> proto --- TODO(bladyjoker): Revisit and make part of compiler.proto -data ProtoError - = MultipleInstanceHeads TyClassRef [Ty] SourceInfo - | NoInstanceHead TyClassRef SourceInfo - | NoConstraintArgs TyClassRef SourceInfo - | MultipleConstraintArgs TyClassRef [Ty] SourceInfo - | NoClassArgs ClassName SourceInfo - | MultipleClassArgs ClassName SourceInfo - | EmptyField - | UnrecognizedKindRefEnum Text - deriving stock (Show, Eq, Ord) - throwNamingError :: Either NamingError b -> FromProto b throwNamingError = either (\err -> throwError [NamingError err]) return @@ -76,9 +73,6 @@ throwOneOfError protoMsgName protoFieldName = & P.oneOfNotSetError . P.fieldName .~ protoFieldName ] -throwProtoError :: ProtoError -> FromProto b -throwProtoError err = throwError [ProtoError err] - throwInternalError :: Text -> FromProto b throwInternalError msg = throwError [InternalError $ defMessage & P.msg .~ msg] @@ -110,6 +104,36 @@ instance IsMessage P.SourceInfo SourceInfo where & P.posFrom .~ toProto (si ^. #posFrom) & P.posTo .~ toProto (si ^. #posTo) +{- + Names +-} + +instance IsMessage Text Text where + fromProto = pure + toProto = id + +instance IsMessage P.ModuleNamePart ModuleNamePart where + fromProto mnp = do + si <- fromProto $ mnp ^. P.sourceInfo + throwNamingError $ checkModuleNamePart mnp + pure $ ModuleNamePart (mnp ^. P.name) si + + toProto (ModuleNamePart nm si) = + defMessage + & P.name .~ nm + & P.sourceInfo .~ toProto si + +instance IsMessage P.ModuleName ModuleName where + fromProto mn = do + si <- fromProto $ mn ^. P.sourceInfo + parts <- traverse fromProto $ mn ^. P.parts + pure $ ModuleName parts si + + toProto (ModuleName parts si) = + defMessage + & P.parts .~ (toProto <$> parts) + & P.sourceInfo .~ toProto si + instance IsMessage P.FieldName FieldName where fromProto v = do throwNamingError $ checkFieldName v @@ -179,7 +203,7 @@ instance IsMessage P.TyApp TyApp where fromProto ta = do tf <- fromProto $ ta ^. P.tyFunc si <- fromProto $ ta ^. P.sourceInfo - targs <- ta ^. (P.tyArgs . traversing fromProto) + targs <- traverse fromProto $ ta ^. P.tyArgs pure $ TyApp tf targs si toProto (TyApp tf args si) = @@ -242,10 +266,15 @@ instance IsMessage P.TyRef TyRef where instance IsMessage P.TyDef TyDef where fromProto td = do - tnm <- fromProto $ td ^. P.tyName - tyabs <- fromProto $ td ^. P.tyAbs - si <- fromProto $ td ^. P.sourceInfo - pure $ TyDef tnm tyabs si + ctx <- ask + ctxModuleName <- case ctx of + CtxModule mn -> return mn + _ -> throwInternalError "Expected to be in Module Context" + local (const $ CtxTyDef ctxModuleName td) $ do + tnm <- fromProto $ td ^. P.tyName + tyabs <- fromProto $ td ^. P.tyAbs + si <- fromProto $ td ^. P.sourceInfo + pure $ TyDef tnm tyabs si toProto (TyDef tnm tyabs si) = defMessage @@ -255,13 +284,18 @@ instance IsMessage P.TyDef TyDef where instance IsMessage P.TyAbs TyAbs where fromProto ta = do - (tyargs, mulTyArgs) <- parseAndIndex (\a -> a ^. #argName) (ta ^. P.tyArgs) + (tyargs, mulTyArgs) <- parseAndIndex (\a -> stripSourceInfo $ a ^. #argName) (ta ^. P.tyArgs) tybody <- fromProto $ ta ^. P.tyBody si <- fromProto $ ta ^. P.sourceInfo + ctx <- ask + (ctxMn, ctxTyd) <- case ctx of + CtxTyDef mn tyd -> return (mn, tyd) + _ -> throwInternalError "Expected to be in TyDef Context" let mulArgsErrs = [ ProtoParseError $ defMessage - -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleTyargError . P.moduleName .~ ctxMn + & P.multipleTyargError . P.tyDef .~ ctxTyd & P.multipleTyargError . P.tyArgs .~ args | (_an, args) <- Map.toList mulTyArgs ] @@ -276,10 +310,19 @@ instance IsMessage P.TyAbs TyAbs where & P.sourceInfo .~ toProto si instance IsMessage P.Kind'KindRef KindRefType where - fromProto = \case - P.Kind'KIND_REF_TYPE -> pure KType - P.Kind'KIND_REF_UNSPECIFIED -> pure KUnspecified - P.Kind'KindRef'Unrecognized v -> throwProtoError $ UnrecognizedKindRefEnum (Text.pack . show $ v) + fromProto kr = + ( \case + P.Kind'KIND_REF_TYPE -> pure KType + P.Kind'KIND_REF_UNSPECIFIED -> pure KUnspecified + P.Kind'KindRef'Unrecognized v -> + throwError + [ ProtoParseError $ + defMessage + & P.unknownEnumError . P.enumName .~ Text.pack (showEnum kr) + & P.unknownEnumError . P.gotTag .~ (Text.pack . show $ v) + ] + ) + kr toProto = \case KType -> P.Kind'KIND_REF_TYPE @@ -330,19 +373,23 @@ instance IsMessage P.TyBody TyBody where instance IsMessage P.Sum Sum where fromProto s = do - (ctors, mulCtors) <- parseAndIndex (\c -> c ^. #constrName) (s ^. P.constructors) + (ctors, mulCtors) <- parseAndIndex (\c -> stripSourceInfo $ c ^. #constrName) (s ^. P.constructors) si <- fromProto $ s ^. P.sourceInfo - -- TODO(bladyjoker): ctors <- maybe (throwProtoError $ EmptySumBody si) return $ nonEmpty ctors' - let mulFieldsErrs = + ctx <- ask + (ctxMn, ctxTyd) <- case ctx of + CtxTyDef mn tyd -> return (mn, tyd) + _ -> throwInternalError "Expected to be in TyDef Context" + let mulCtorsErrs = [ ProtoParseError $ defMessage - -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleConstructorError . P.moduleName .~ ctxMn + & P.multipleConstructorError . P.tyDef .~ ctxTyd & P.multipleConstructorError . P.constructors .~ cs | (_cn, cs) <- Map.toList mulCtors ] - if null mulFieldsErrs + if null mulCtorsErrs then pure $ Sum ctors si - else throwError mulFieldsErrs + else throwError mulCtorsErrs toProto (Sum ctors si) = defMessage @@ -362,12 +409,17 @@ instance IsMessage P.Sum'Constructor Constructor where instance IsMessage P.Product'Record Record where fromProto r = do - (fields, mulFields) <- parseAndIndex (\f -> f ^. #fieldName) (r ^. P.fields) + (fields, mulFields) <- parseAndIndex (\f -> stripSourceInfo $ f ^. #fieldName) (r ^. P.fields) si <- fromProto $ r ^. P.sourceInfo + ctx <- ask + (ctxMn, ctxTyd) <- case ctx of + CtxTyDef mn tyd -> return (mn, tyd) + _ -> throwInternalError "Expected to be in TyDef Context" let mulFieldsErrs = [ ProtoParseError $ defMessage - -- TODO(bladyjoker): Add Module/TyDef context + & P.multipleFieldError . P.moduleName .~ ctxMn + & P.multipleFieldError . P.tyDef .~ ctxTyd & P.multipleFieldError . P.fields .~ fs | (_fn, fs) <- Map.toList mulFields ] @@ -459,16 +511,21 @@ instance IsMessage P.TyClassRef TyClassRef where instance IsMessage P.ClassDef ClassDef where fromProto cd = do - si <- fromProto $ cd ^. P.sourceInfo - cnm <- fromProto $ cd ^. P.className - cargs <- traverse fromProto $ cd ^. P.classArgs - carg <- case cargs of - [] -> throwProtoError $ NoClassArgs cnm si - [x] -> return x - _ -> throwInternalError "Multi parameter type classes are not supported" - sups <- traverse fromProto $ cd ^. P.supers - let doc = cd ^. P.documentation - pure $ ClassDef cnm carg sups doc si + ctx <- ask + ctxMn <- case ctx of + CtxModule mn -> return mn + _ -> throwInternalError "Expected to be in Module Context" + local (const $ CtxClassDef ctxMn cd) $ do + si <- fromProto $ cd ^. P.sourceInfo + cnm <- fromProto $ cd ^. P.className + cargs <- traverse fromProto $ cd ^. P.classArgs + carg <- case cargs of + [] -> throwInternalError "Zero parameter type classes are not supported" + [x] -> return x + _ -> throwInternalError "Multi parameter type classes are not supported" + sups <- traverse fromProto $ cd ^. P.supers + let doc = cd ^. P.documentation + pure $ ClassDef cnm carg sups doc si toProto (ClassDef cnm carg sups doc si) = defMessage @@ -483,17 +540,17 @@ instance IsMessage P.InstanceClause InstanceClause where si <- fromProto $ ic ^. P.sourceInfo cnm <- fromProto $ ic ^. P.classRef csts <- traverse fromProto $ ic ^. P.constraints - hds <- ic ^. (P.heads . traversing fromProto) - hd <- case hds of - [] -> throwProtoError $ NoInstanceHead cnm si + args <- traverse fromProto $ ic ^. P.args + arg <- case args of + [] -> throwInternalError "Zero instance arguments, but zero parameter type classes are not supported" [x] -> return x - _ -> throwInternalError "Multiple instance head, but multi parameter type classes are not supported" - pure $ InstanceClause cnm hd csts si + _ -> throwInternalError "Multiple instance arguments, but multi parameter type classes are not supported" + pure $ InstanceClause cnm arg csts si toProto (InstanceClause cnm hd csts si) = defMessage & P.classRef .~ toProto cnm - & P.heads .~ pure (toProto hd) + & P.args .~ pure (toProto hd) & P.constraints .~ (toProto <$> csts) & P.sourceInfo .~ toProto si @@ -501,11 +558,11 @@ instance IsMessage P.Constraint Constraint where fromProto c = do si <- fromProto $ c ^. P.sourceInfo cnm <- fromProto $ c ^. P.classRef - args <- c ^. (P.arguments . traversing fromProto) + args <- traverse fromProto $ c ^. P.arguments arg <- case args of - [] -> throwProtoError $ NoConstraintArgs cnm si + [] -> throwInternalError "Zero constraint arguments, but zero parameter type classes are not supported" [x] -> return x - _ -> throwInternalError "Multiple instance constraint arguments, but multi parameter type classes are not supported" + _ -> throwInternalError "Multiple constraint arguments, but multi parameter type classes are not supported" pure $ Constraint cnm arg si toProto (Constraint cnm arg si) = @@ -523,45 +580,54 @@ parseAndIndex key = foldlM ( \(indexed, multiples) px -> do x <- fromProto px - if Map.member (key x) indexed - then return (indexed, Map.insertWith (++) (key x) [px] multiples) - else return (Map.insert (key x) x indexed, multiples) + let k = key x + if Map.member k indexed + then return (indexed, Map.insertWith (++) k [px] multiples) + else return (Map.insert k x indexed, multiples) ) (mempty, mempty) +stripSourceInfo :: HasField "sourceInfo" s t a SourceInfo => s -> t +stripSourceInfo x = x & #sourceInfo .~ defSourceInfo + instance IsMessage P.Module Module where fromProto m = do - mnm <- fromProto $ m ^. P.moduleName - (tydefs, mulTyDefs) <- parseAndIndex (\tyDef -> tyDef ^. #tyName) (m ^. P.typeDefs) - (cldefs, mulClDefs) <- parseAndIndex (\cldef -> cldef ^. #className) (m ^. P.classDefs) - (impts, mulImpts) <- parseAndIndex (\(mn :: ModuleName) -> mn) (m ^. P.imports) - insts <- traverse fromProto $ m ^. P.instances - si <- fromProto $ m ^. P.sourceInfo - let mulTyDefsErrs = - [ ProtoParseError $ - defMessage - & P.multipleTydefError . P.moduleName .~ (m ^. P.moduleName) - & P.multipleTydefError . P.tyDefs .~ tds - | (_tn, tds) <- Map.toList mulTyDefs - ] - mulClassDefsErrs = - [ ProtoParseError $ - defMessage - & P.multipleClassdefError . P.moduleName .~ (m ^. P.moduleName) - & P.multipleClassdefError . P.classDefs .~ cds - | (_cn, cds) <- Map.toList mulClDefs - ] - mulImptsErrs = - [ ProtoParseError $ - defMessage - & P.multipleImportError . P.moduleName .~ (m ^. P.moduleName) - & P.multipleImportError . P.imports .~ ims - | (_in, ims) <- Map.toList mulImpts - ] - protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs ++ mulImptsErrs - if null protoParseErrs - then pure $ Module mnm tydefs cldefs insts (Map.keysSet impts) si - else throwError protoParseErrs + ctx <- ask + case ctx of + CtxCompilerInput -> return () + _ -> throwInternalError "Expected to be in CompilerInput Context" + local (const $ CtxModule (m ^. P.moduleName)) $ do + mnm <- fromProto $ m ^. P.moduleName + (tydefs, mulTyDefs) <- parseAndIndex (\tyDef -> stripSourceInfo $ tyDef ^. #tyName) (m ^. P.typeDefs) + (cldefs, mulClDefs) <- parseAndIndex (\cldef -> stripSourceInfo $ cldef ^. #className) (m ^. P.classDefs) + (impts, mulImpts) <- parseAndIndex stripSourceInfo (m ^. P.imports) + insts <- traverse fromProto $ m ^. P.instances + si <- fromProto $ m ^. P.sourceInfo + let mulTyDefsErrs = + [ ProtoParseError $ + defMessage + & P.multipleTydefError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleTydefError . P.tyDefs .~ tds + | (_tn, tds) <- Map.toList mulTyDefs + ] + mulClassDefsErrs = + [ ProtoParseError $ + defMessage + & P.multipleClassdefError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleClassdefError . P.classDefs .~ cds + | (_cn, cds) <- Map.toList mulClDefs + ] + mulImptsErrs = + [ ProtoParseError $ + defMessage + & P.multipleImportError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleImportError . P.imports .~ ims + | (_in, ims) <- Map.toList mulImpts + ] + protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs ++ mulImptsErrs + if null protoParseErrs + then pure $ Module mnm tydefs cldefs insts (Map.keysSet impts) si + else throwError protoParseErrs toProto (Module mnm tdefs cdefs insts impts si) = defMessage @@ -574,52 +640,21 @@ instance IsMessage P.Module Module where instance IsMessage P.CompilerInput CompilerInput where fromProto ci = do - (mods, mulModules) <- parseAndIndex (\m -> m ^. #moduleName) (ci ^. P.modules) - let mulModulesErrs = - [ ProtoParseError $ - defMessage - -- TODO(bladyjoker): Add Module/TyDef context - & P.multipleModuleError . P.modules .~ ms - | (_mn, ms) <- Map.toList mulModules - ] - if null mulModulesErrs - then pure $ CompilerInput mods - else throwError mulModulesErrs + local (const CtxCompilerInput) $ do + (mods, mulModules) <- parseAndIndex (\m -> stripSourceInfo $ m ^. #moduleName) (ci ^. P.modules) + let mulModulesErrs = + [ ProtoParseError $ + defMessage & P.multipleModuleError . P.modules .~ ms + | (_mn, ms) <- Map.toList mulModules + ] + if null mulModulesErrs + then pure $ CompilerInput mods + else throwError mulModulesErrs toProto (CompilerInput ms) = defMessage & P.modules .~ (toProto <$> toList ms) -{- - Names --} - -instance IsMessage Text Text where - fromProto = pure - toProto = id - -instance IsMessage P.ModuleNamePart ModuleNamePart where - fromProto mnp = do - nm <- fromProto $ mnp ^. P.name - si <- fromProto $ mnp ^. P.sourceInfo - pure $ ModuleNamePart nm si - - toProto (ModuleNamePart nm si) = - defMessage - & P.name .~ nm - & P.sourceInfo .~ toProto si - -instance IsMessage P.ModuleName ModuleName where - fromProto mn = do - si <- fromProto $ mn ^. P.sourceInfo - parts <- traverse fromProto $ mn ^. P.parts - pure $ ModuleName parts si - - toProto (ModuleName parts si) = - defMessage - & P.parts .~ (toProto <$> parts) - & P.sourceInfo .~ toProto si - {- Outputs -} @@ -645,7 +680,7 @@ instance IsMessage P.KindCheckError KindCheckError where <$> fromProto (err ^. P.tyName) <*> fromProto (err ^. P.inferredKind) <*> fromProto (err ^. P.definedKind) - Nothing -> throwProtoError EmptyField + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckError)) "kind_check_error" toProto = \case UnboundTermError tyname varname -> diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index eea25264..617ae009 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -48,6 +48,7 @@ module LambdaBuffers.Compiler.ProtoCompat.Types ( TyVar (..), VarName (..), module VARS, + defSourceInfo, ) where import Control.Exception (Exception) @@ -68,6 +69,9 @@ data SourcePosition = SourcePosition {column :: Int, row :: Int} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary SourcePosition +defSourceInfo :: SourceInfo +defSourceInfo = SourceInfo "" (SourcePosition 0 0) (SourcePosition 0 0) + {- | NOTE(gnumonik): I need a "generic name" type for my template haskell, this shouldn't be used anywhere outside of that -} diff --git a/lambda-buffers-compiler/test/Test/TypeClassCheck.hs b/lambda-buffers-compiler/test/Test/TypeClassCheck.hs index 6363deef..547ae852 100644 --- a/lambda-buffers-compiler/test/Test/TypeClassCheck.hs +++ b/lambda-buffers-compiler/test/Test/TypeClassCheck.hs @@ -1,17 +1,19 @@ module Test.TypeClassCheck (test) where -import Control.Lens ((.~)) +import Control.Lens ((.~), (^.)) +import Data.Foldable (Foldable (toList)) import Data.Function ((&)) +import Data.Map qualified as Map import Data.ProtoLens (Message (defMessage)) import Data.Text (Text) -import Data.Traversable (for) -import LambdaBuffers.Compiler.ProtoCompat (IsMessage (fromProto)) +import LambdaBuffers.Compiler.ProtoCompat (runFromProto) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as ProtoCompat import LambdaBuffers.Compiler.TypeClassCheck (detectSuperclassCycles') -import Proto.Compiler (ClassDef, Constraint, Kind, Kind'KindRef (Kind'KIND_REF_TYPE)) -import Proto.Compiler_Fields (argKind, argName, arguments, classArgs, className, classRef, kindRef, localClassRef, name, supers, tyVar, varName) +import Proto.Compiler (ClassDef, CompilerInput, Constraint, Kind, Kind'KindRef (Kind'KIND_REF_TYPE)) +import Proto.Compiler_Fields (argKind, argName, arguments, classArgs, classDefs, className, classRef, kindRef, localClassRef, moduleName, modules, name, parts, supers, tyVar, varName) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertFailure, testCase, (@?=)) +import Test.Utils.Constructors (_ModuleName) test :: TestTree test = @@ -24,17 +26,25 @@ test = noCycleDetected :: TestTree noCycleDetected = testCase "No cycle detected" $ do - nocycles' <- classDefsFromProto nocycles - detectSuperclassCycles' nocycles' @?= [] + nocycles' <- fromProto' nocycles + case Map.lookup (_ModuleName ["ModuleWithNoClassCycles"]) (nocycles' ^. #modules) of + Nothing -> assertFailure "Failed lookup to ModuleWithClassNoClassCycles" + Just m -> detectSuperclassCycles' (toList $ m ^. #classDefs) @?= [] cycleDetected :: TestTree cycleDetected = testCase "Cycle detected" $ do - cycles' <- classDefsFromProto cycles - detectSuperclassCycles' cycles' @?= [["Bar", "Foo", "Bop", "Bar"], ["Bop", "Bar", "Foo", "Bop"], ["Foo", "Bop", "Bar", "Foo"]] + cycles' <- fromProto' cycles + case Map.lookup (_ModuleName ["ModuleWithClassCycles"]) (cycles' ^. #modules) of + Nothing -> assertFailure "Failed lookup to ModuleWithClassCycles" + Just m -> detectSuperclassCycles' (toList $ m ^. #classDefs) @?= [["Bar", "Foo", "Bop", "Bar"], ["Bop", "Bar", "Foo", "Bop"], ["Foo", "Bop", "Bar", "Foo"]] -classDefsFromProto :: [ClassDef] -> IO [ProtoCompat.ClassDef] -classDefsFromProto cds = for cds (either (\err -> assertFailure $ "FromProto failed with " <> show err) return . fromProto @ClassDef @ProtoCompat.ClassDef) +fromProto' :: CompilerInput -> IO ProtoCompat.CompilerInput +fromProto' compInp = + either + (\errs -> assertFailure $ "FromProto failed with " <> show errs) + return + (runFromProto compInp) star :: Kind star = defMessage & kindRef .~ Kind'KIND_REF_TYPE @@ -56,17 +66,29 @@ constraint nm = & classRef . localClassRef . className . name .~ nm & arguments .~ [defMessage & tyVar . varName . name .~ "a"] -cycles :: [ClassDef] +cycles :: CompilerInput cycles = - [ mkclass "Foo" ["Bar", "Baz", "Beep"] - , mkclass "Bar" ["Bip", "Bop"] - , mkclass "Bop" ["Foo"] - ] + defMessage + & modules + .~ [ defMessage + & moduleName . parts .~ [defMessage & name .~ "ModuleWithClassCycles"] + & classDefs + .~ [ mkclass "Foo" ["Bar", "Baz", "Beep"] + , mkclass "Bar" ["Bip", "Bop"] + , mkclass "Bop" ["Foo"] + ] + ] -nocycles :: [ClassDef] +nocycles :: CompilerInput nocycles = - [ mkclass "Functor" [] - , mkclass "Applicative" ["Functor"] - , mkclass "Monad" ["Applicative"] - , mkclass "Traversable" ["Foldable", "Functor"] - ] + defMessage + & modules + .~ [ defMessage + & moduleName . parts .~ [defMessage & name .~ "ModuleWithNoClassCycles"] + & classDefs + .~ [ mkclass "Functor" [] + , mkclass "Applicative" ["Functor"] + , mkclass "Monad" ["Applicative"] + , mkclass "Traversable" ["Foldable", "Functor"] + ] + ] diff --git a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs index 12101c2c..d52c0980 100644 --- a/lambda-buffers-compiler/test/Test/Utils/Constructors.hs +++ b/lambda-buffers-compiler/test/Test/Utils/Constructors.hs @@ -22,7 +22,6 @@ import Control.Lens ((^.)) import Data.Map qualified as Map import Data.Text (Text) import LambdaBuffers.Compiler.ProtoCompat qualified as P -import Test.Utils.SourceInfo (sourceInfo'empty) _CompilerInput :: [P.Module] -> P.CompilerInput _CompilerInput ms = @@ -38,37 +37,37 @@ _Module mn tds cds ins = , P.classDefs = Map.fromList [(cd ^. #className, cd) | cd <- cds] , P.instances = ins , P.imports = mempty - , P.sourceInfo = sourceInfo'empty + , P.sourceInfo = P.defSourceInfo } _ModuleName :: [Text] -> P.ModuleName _ModuleName ps = P.ModuleName { P.parts = _ModuleNamePart <$> ps - , P.sourceInfo = sourceInfo'empty + , P.sourceInfo = P.defSourceInfo } _ModuleNamePart :: Text -> P.ModuleNamePart -_ModuleNamePart n = P.ModuleNamePart n sourceInfo'empty +_ModuleNamePart n = P.ModuleNamePart n P.defSourceInfo _tyName :: Text -> P.TyName -_tyName x = P.TyName x sourceInfo'empty +_tyName x = P.TyName x P.defSourceInfo _varName :: Text -> P.VarName -_varName x = P.VarName {P.name = x, P.sourceInfo = sourceInfo'empty} +_varName x = P.VarName {P.name = x, P.sourceInfo = P.defSourceInfo} _tyVar :: Text -> P.TyVar -_tyVar x = P.TyVar {P.varName = _varName x, P.sourceInfo = sourceInfo'empty} +_tyVar x = P.TyVar {P.varName = _varName x, P.sourceInfo = P.defSourceInfo} _TyVarI :: Text -> P.Ty -_TyVarI x = P.TyVarI $ P.TyVar {P.varName = _varName x, P.sourceInfo = sourceInfo'empty} +_TyVarI x = P.TyVarI $ P.TyVar {P.varName = _varName x, P.sourceInfo = P.defSourceInfo} _TupleI :: [P.Ty] -> P.Product _TupleI x = P.TupleI $ P.Tuple { P.fields = x - , P.sourceInfo = sourceInfo'empty + , P.sourceInfo = P.defSourceInfo } _Constructor :: Text -> P.Product -> P.Constructor @@ -82,7 +81,7 @@ _ConstrName :: Text -> P.ConstrName _ConstrName x = P.ConstrName { P.name = x - , P.sourceInfo = sourceInfo'empty + , P.sourceInfo = P.defSourceInfo } _Sum :: [(Text, P.Product)] -> P.TyBody @@ -90,7 +89,7 @@ _Sum cs = P.SumI $ P.Sum { constructors = Map.fromList [(ctor ^. #constrName, ctor) | (cn, cp) <- cs, ctor <- [_Constructor cn cp]] - , sourceInfo = sourceInfo'empty + , sourceInfo = P.defSourceInfo } _TyAbs :: [(Text, P.KindType)] -> [(Text, P.Product)] -> P.TyAbs @@ -98,28 +97,28 @@ _TyAbs args body = P.TyAbs { P.tyArgs = Map.fromList [(ta ^. #argName, ta) | ta <- _TyArg <$> args] , P.tyBody = _Sum body - , sourceInfo = sourceInfo'empty + , sourceInfo = P.defSourceInfo } _TyArg :: (Text, P.KindType) -> P.TyArg _TyArg (a, k) = P.TyArg - { P.argName = P.VarName a sourceInfo'empty + { P.argName = P.VarName a P.defSourceInfo , P.argKind = P.Kind {P.kind = k} - , P.sourceInfo = sourceInfo'empty + , P.sourceInfo = P.defSourceInfo } _Type :: P.KindType _Type = P.KindRef P.KType _TyDef :: P.TyName -> P.TyAbs -> P.TyDef -_TyDef name ab = P.TyDef {P.tyName = name, P.tyAbs = ab, sourceInfo = sourceInfo'empty} +_TyDef name ab = P.TyDef {P.tyName = name, P.tyAbs = ab, sourceInfo = P.defSourceInfo} _TyRefILocal :: Text -> P.Ty _TyRefILocal x = P.TyRefI $ P.LocalI $ P.LocalRef - { P.tyName = P.TyName {P.name = x, P.sourceInfo = sourceInfo'empty} - , P.sourceInfo = sourceInfo'empty + { P.tyName = P.TyName {P.name = x, sourceInfo = P.defSourceInfo} + , P.sourceInfo = P.defSourceInfo } diff --git a/lambda-buffers-compiler/test/Test/Utils/SourceInfo.hs b/lambda-buffers-compiler/test/Test/Utils/SourceInfo.hs deleted file mode 100644 index cb04608b..00000000 --- a/lambda-buffers-compiler/test/Test/Utils/SourceInfo.hs +++ /dev/null @@ -1,7 +0,0 @@ -module Test.Utils.SourceInfo (sourceInfo'empty) where - -import LambdaBuffers.Compiler.ProtoCompat qualified as P - --- | Empty Source Info -sourceInfo'empty :: P.SourceInfo -sourceInfo'empty = P.SourceInfo "Empty Info" (P.SourcePosition 0 0) (P.SourcePosition 0 1) diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index 7aad5932..74f577a0 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -452,17 +452,16 @@ message TyClassRef { } } -/* Type class instances +/* Type class instances (rules) Instance clauses enable users to specify 'semantic' rules for their types. */ message InstanceClause { // Type class name. TyClassRef class_ref = 1; - // Head of the instance clause. Currently, the Compiler only accepts single - // parameter type classes. - repeated Ty heads = 2; - // Body of the rule, conjunction of constraints. + // Instance (rule) arguments. + repeated Ty args = 2; + // Instance (rule) body, conjunction of constraints. repeated Constraint constraints = 3; // Source information. SourceInfo source_info = 4; @@ -591,10 +590,10 @@ message ProtoParseError { // Proto `enum` field is unknown. message UnknownEnumError { - // Proto message name in which the `enum` field is unknown. - string message_name = 1; - // The `enum` field that is unknown. - string field_name = 2; + // Proto `enum` name. + string enum_name = 1; + // The unknown tag for the `enum`. + string got_tag = 2; } oneof proto_parse_error { From e052e325bca6d40d0ee9781591267d90a50e2991 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 12:30:57 +0100 Subject: [PATCH 09/20] Reshuffle into ProtoCompat/FromProto --- .../lambda-buffers-compiler.cabal | 1 + .../src/LambdaBuffers/Compiler/ProtoCompat.hs | 744 +----------------- .../Compiler/ProtoCompat/FromProto.hs | 738 +++++++++++++++++ 3 files changed, 743 insertions(+), 740 deletions(-) create mode 100644 lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index 3980a239..7837faa1 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -117,6 +117,7 @@ library LambdaBuffers.Compiler.KindCheck.Variable LambdaBuffers.Compiler.NamingCheck LambdaBuffers.Compiler.ProtoCompat + LambdaBuffers.Compiler.ProtoCompat.FromProto LambdaBuffers.Compiler.ProtoCompat.Types LambdaBuffers.Compiler.TypeClass.Pat LambdaBuffers.Compiler.TypeClass.Pretty diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs index 60bfdcf6..905e3508 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat.hs @@ -1,745 +1,9 @@ {-# OPTIONS_GHC -Wno-missing-import-lists #-} -{-# OPTIONS_GHC -Wno-redundant-constraints #-} module LambdaBuffers.Compiler.ProtoCompat ( - IsMessage (..), - FromProtoErr (..), - module X, - protoKind2Kind, - kind2ProtoKind, - runFromProto, + module FromProto, + module Types, ) where --- NOTE(cstml): I'm re-exporting the module from here as it makes more sense - --- also avoids annoying errors. -import LambdaBuffers.Compiler.ProtoCompat.Types as X hiding (InternalError) - -import Control.Lens ((&), (.~), (^.)) -import Control.Monad.Except (Except, MonadError (throwError), runExcept) -import Control.Monad.Reader (MonadReader (ask, local), ReaderT (runReaderT)) -import Data.Foldable (foldlM, toList) -import Data.Generics.Labels () -import Data.Generics.Product (HasField) -import Data.Kind (Type) -import Data.Map (Map) -import Data.Map qualified as Map -import Data.ProtoLens (Message (messageName), MessageEnum (showEnum), defMessage) -import Data.Proxy (Proxy (Proxy)) -import Data.Set qualified as Set -import Data.Text (Text) -import Data.Text qualified as Text -import GHC.Generics (Generic) -import LambdaBuffers.Compiler.KindCheck.Kind qualified as K -import LambdaBuffers.Compiler.NamingCheck (checkClassName, checkConstrName, checkFieldName, checkModuleNamePart, checkTyName, checkVarName) -import Proto.Compiler (NamingError) -import Proto.Compiler qualified as P -import Proto.Compiler_Fields qualified as P - -data FromProtoErr - = NamingError P.NamingError - | InternalError P.InternalError - | ProtoParseError P.ProtoParseError - deriving stock (Show, Eq, Ord, Generic) - -data FromProtoContext - = CtxCompilerInput - | CtxModule P.ModuleName - | CtxTyDef P.ModuleName P.TyDef - | CtxClassDef P.ModuleName P.ClassDef - deriving stock (Show, Eq, Ord, Generic) - -type FromProto a = ReaderT FromProtoContext (Except [FromProtoErr]) a - --- | Parse a Proto API CompilerInput into the internal CompilerInput representation or report errors. -runFromProto :: P.CompilerInput -> Either [FromProtoErr] CompilerInput -runFromProto compInp = do - let exM = runReaderT (fromProto compInp) CtxCompilerInput - runExcept exM - -class IsMessage (proto :: Type) (good :: Type) where - fromProto :: proto -> FromProto good - - toProto :: good -> proto - -throwNamingError :: Either NamingError b -> FromProto b -throwNamingError = either (\err -> throwError [NamingError err]) return - -throwOneOfError :: Text -> Text -> FromProto b -throwOneOfError protoMsgName protoFieldName = - throwError - [ ProtoParseError $ - defMessage - & P.oneOfNotSetError . P.messageName .~ protoMsgName - & P.oneOfNotSetError . P.fieldName .~ protoFieldName - ] - -throwInternalError :: Text -> FromProto b -throwInternalError msg = throwError [InternalError $ defMessage & P.msg .~ msg] - -{- - SourceInfo --} - -instance IsMessage P.SourcePosition SourcePosition where - fromProto sp = do - let col = fromIntegral $ sp ^. P.column - row = fromIntegral $ sp ^. P.row - pure $ SourcePosition col row - - toProto sp = - defMessage - & P.column .~ fromIntegral (sp ^. #column) - & P.row .~ fromIntegral (sp ^. #row) - -instance IsMessage P.SourceInfo SourceInfo where - fromProto si = do - let file = si ^. P.file - pFrom <- fromProto $ si ^. P.posFrom - pTo <- fromProto $ si ^. P.posTo - pure $ SourceInfo file pFrom pTo - - toProto si = - defMessage - & P.file .~ (si ^. #file) - & P.posFrom .~ toProto (si ^. #posFrom) - & P.posTo .~ toProto (si ^. #posTo) - -{- - Names --} - -instance IsMessage Text Text where - fromProto = pure - toProto = id - -instance IsMessage P.ModuleNamePart ModuleNamePart where - fromProto mnp = do - si <- fromProto $ mnp ^. P.sourceInfo - throwNamingError $ checkModuleNamePart mnp - pure $ ModuleNamePart (mnp ^. P.name) si - - toProto (ModuleNamePart nm si) = - defMessage - & P.name .~ nm - & P.sourceInfo .~ toProto si - -instance IsMessage P.ModuleName ModuleName where - fromProto mn = do - si <- fromProto $ mn ^. P.sourceInfo - parts <- traverse fromProto $ mn ^. P.parts - pure $ ModuleName parts si - - toProto (ModuleName parts si) = - defMessage - & P.parts .~ (toProto <$> parts) - & P.sourceInfo .~ toProto si - -instance IsMessage P.FieldName FieldName where - fromProto v = do - throwNamingError $ checkFieldName v - FieldName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) - - toProto (FieldName n si) = - defMessage - & P.name .~ toProto n - & P.sourceInfo .~ toProto si - -instance IsMessage P.ConstrName ConstrName where - fromProto v = do - throwNamingError $ checkConstrName v - ConstrName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) - - toProto (ConstrName n si) = - defMessage - & P.name .~ toProto n - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyName TyName where - fromProto v = do - throwNamingError $ checkTyName v - TyName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) - - toProto (TyName n si) = - defMessage - & P.name .~ toProto n - & P.sourceInfo .~ toProto si - -instance IsMessage P.ClassName ClassName where - fromProto v = do - throwNamingError $ checkClassName v - ClassName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) - - toProto (ClassName n si) = - defMessage - & P.name .~ toProto n - & P.sourceInfo .~ toProto si - -instance IsMessage P.VarName VarName where - fromProto v = do - throwNamingError $ checkVarName v - VarName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) - - toProto (VarName n si) = - defMessage - & P.name .~ toProto n - & P.sourceInfo .~ toProto si - -{- - Ty & Components --} - -instance IsMessage P.TyVar TyVar where - fromProto tv = do - vn <- fromProto $ tv ^. P.varName - si <- fromProto $ tv ^. P.sourceInfo - pure $ TyVar vn si - - toProto (TyVar vn si) = - defMessage - & P.varName .~ toProto vn - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyApp TyApp where - fromProto ta = do - tf <- fromProto $ ta ^. P.tyFunc - si <- fromProto $ ta ^. P.sourceInfo - targs <- traverse fromProto $ ta ^. P.tyArgs - pure $ TyApp tf targs si - - toProto (TyApp tf args si) = - defMessage - & P.tyFunc .~ toProto tf - & P.tyArgs .~ toList (toProto <$> args) - & P.sourceInfo .~ toProto si - -instance IsMessage P.Ty Ty where - fromProto ti = case ti ^. P.maybe'ty of - Nothing -> throwOneOfError (messageName (Proxy @P.Ty)) "ty" - Just x -> case x of - P.Ty'TyVar tv -> TyVarI <$> fromProto tv - P.Ty'TyApp ta -> TyAppI <$> fromProto ta - P.Ty'TyRef tr -> TyRefI <$> fromProto tr - - toProto = \case - TyVarI tv -> defMessage & P.tyVar .~ toProto tv - TyRefI tr -> defMessage & P.tyRef .~ toProto tr - TyAppI ta -> defMessage & P.tyApp .~ toProto ta - -instance IsMessage P.TyRef'Local LocalRef where - fromProto lr = do - si <- fromProto $ lr ^. P.sourceInfo - nm <- fromProto $ lr ^. P.tyName - pure $ LocalRef nm si - - toProto (LocalRef nm si) = - defMessage - & P.tyName .~ toProto nm - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyRef'Foreign ForeignRef where - fromProto fr = do - si <- fromProto $ fr ^. P.sourceInfo - mn <- fromProto $ fr ^. P.moduleName - tn <- fromProto $ fr ^. P.tyName - pure $ ForeignRef tn mn si - - toProto (ForeignRef tn mn si) = - defMessage - & P.tyName .~ toProto tn - & P.moduleName .~ toProto mn - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyRef TyRef where - fromProto tr = case tr ^. P.maybe'tyRef of - Nothing -> throwOneOfError (messageName (Proxy @P.TyRef)) "ty_ref" - Just x -> case x of - P.TyRef'LocalTyRef lr -> LocalI <$> fromProto lr - P.TyRef'ForeignTyRef f -> ForeignI <$> fromProto f - - toProto = \case - LocalI lr -> defMessage & P.localTyRef .~ toProto lr - ForeignI fr -> defMessage & P.foreignTyRef .~ toProto fr - -{- - TyDef & Components --} - -instance IsMessage P.TyDef TyDef where - fromProto td = do - ctx <- ask - ctxModuleName <- case ctx of - CtxModule mn -> return mn - _ -> throwInternalError "Expected to be in Module Context" - local (const $ CtxTyDef ctxModuleName td) $ do - tnm <- fromProto $ td ^. P.tyName - tyabs <- fromProto $ td ^. P.tyAbs - si <- fromProto $ td ^. P.sourceInfo - pure $ TyDef tnm tyabs si - - toProto (TyDef tnm tyabs si) = - defMessage - & P.tyName .~ toProto tnm - & P.tyAbs .~ toProto tyabs - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyAbs TyAbs where - fromProto ta = do - (tyargs, mulTyArgs) <- parseAndIndex (\a -> stripSourceInfo $ a ^. #argName) (ta ^. P.tyArgs) - tybody <- fromProto $ ta ^. P.tyBody - si <- fromProto $ ta ^. P.sourceInfo - ctx <- ask - (ctxMn, ctxTyd) <- case ctx of - CtxTyDef mn tyd -> return (mn, tyd) - _ -> throwInternalError "Expected to be in TyDef Context" - let mulArgsErrs = - [ ProtoParseError $ - defMessage - & P.multipleTyargError . P.moduleName .~ ctxMn - & P.multipleTyargError . P.tyDef .~ ctxTyd - & P.multipleTyargError . P.tyArgs .~ args - | (_an, args) <- Map.toList mulTyArgs - ] - if null mulArgsErrs - then pure $ TyAbs tyargs tybody si - else throwError mulArgsErrs - - toProto (TyAbs tyargs tyabs si) = - defMessage - & P.tyArgs .~ (toProto <$> toList tyargs) - & P.tyBody .~ toProto tyabs - & P.sourceInfo .~ toProto si - -instance IsMessage P.Kind'KindRef KindRefType where - fromProto kr = - ( \case - P.Kind'KIND_REF_TYPE -> pure KType - P.Kind'KIND_REF_UNSPECIFIED -> pure KUnspecified - P.Kind'KindRef'Unrecognized v -> - throwError - [ ProtoParseError $ - defMessage - & P.unknownEnumError . P.enumName .~ Text.pack (showEnum kr) - & P.unknownEnumError . P.gotTag .~ (Text.pack . show $ v) - ] - ) - kr - - toProto = \case - KType -> P.Kind'KIND_REF_TYPE - KUnspecified -> P.Kind'KIND_REF_UNSPECIFIED - -instance IsMessage P.Kind Kind where - fromProto k = do - kt <- case k ^. P.maybe'kind of - Nothing -> throwOneOfError (messageName (Proxy @P.Kind)) "kind" - Just k' -> case k' of - P.Kind'KindRef r -> KindRef <$> fromProto r - P.Kind'KindArrow' arr -> KindArrow <$> fromProto (arr ^. P.left) <*> fromProto (arr ^. P.right) - pure $ Kind kt - - toProto (Kind (KindArrow l r)) = do - defMessage - & P.kindArrow . P.left .~ toProto l - & P.kindArrow . P.right .~ toProto r - toProto (Kind (KindRef r)) = do - defMessage - & P.kindRef .~ toProto r - -instance IsMessage P.TyArg TyArg where - fromProto ta = do - argnm <- fromProto $ ta ^. P.argName - si <- fromProto $ ta ^. P.sourceInfo - kind <- fromProto $ ta ^. P.argKind - pure $ TyArg argnm kind si - - toProto (TyArg argnm argkind si) = - defMessage - & P.argName .~ toProto argnm - & P.argKind .~ toProto argkind - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyBody TyBody where - fromProto tb = case tb ^. P.maybe'tyBody of - Nothing -> throwOneOfError (messageName (Proxy @P.TyBody)) "ty_body" - Just x -> case x of - P.TyBody'Opaque opq -> OpaqueI <$> fromProto (opq ^. P.sourceInfo) - P.TyBody'Sum sumI -> SumI <$> fromProto sumI - - toProto = \case - OpaqueI si -> - let opaque = defMessage & P.sourceInfo .~ toProto si - in defMessage & P.opaque .~ opaque - SumI sb -> defMessage & P.sum .~ toProto sb - -instance IsMessage P.Sum Sum where - fromProto s = do - (ctors, mulCtors) <- parseAndIndex (\c -> stripSourceInfo $ c ^. #constrName) (s ^. P.constructors) - si <- fromProto $ s ^. P.sourceInfo - ctx <- ask - (ctxMn, ctxTyd) <- case ctx of - CtxTyDef mn tyd -> return (mn, tyd) - _ -> throwInternalError "Expected to be in TyDef Context" - let mulCtorsErrs = - [ ProtoParseError $ - defMessage - & P.multipleConstructorError . P.moduleName .~ ctxMn - & P.multipleConstructorError . P.tyDef .~ ctxTyd - & P.multipleConstructorError . P.constructors .~ cs - | (_cn, cs) <- Map.toList mulCtors - ] - if null mulCtorsErrs - then pure $ Sum ctors si - else throwError mulCtorsErrs - - toProto (Sum ctors si) = - defMessage - & P.constructors .~ toList (toProto <$> ctors) - & P.sourceInfo .~ toProto si - -instance IsMessage P.Sum'Constructor Constructor where - fromProto c = do - cnm <- fromProto $ c ^. P.constrName - prod <- fromProto $ c ^. P.product - pure $ Constructor cnm prod - - toProto (Constructor cnm prod) = - defMessage - & P.constrName .~ toProto cnm - & P.product .~ toProto prod - -instance IsMessage P.Product'Record Record where - fromProto r = do - (fields, mulFields) <- parseAndIndex (\f -> stripSourceInfo $ f ^. #fieldName) (r ^. P.fields) - si <- fromProto $ r ^. P.sourceInfo - ctx <- ask - (ctxMn, ctxTyd) <- case ctx of - CtxTyDef mn tyd -> return (mn, tyd) - _ -> throwInternalError "Expected to be in TyDef Context" - let mulFieldsErrs = - [ ProtoParseError $ - defMessage - & P.multipleFieldError . P.moduleName .~ ctxMn - & P.multipleFieldError . P.tyDef .~ ctxTyd - & P.multipleFieldError . P.fields .~ fs - | (_fn, fs) <- Map.toList mulFields - ] - if null mulFieldsErrs - then pure $ Record fields si - else throwError mulFieldsErrs - - toProto (Record fs si) = - defMessage - & P.fields .~ (toProto <$> toList fs) - & P.sourceInfo .~ toProto si - -instance IsMessage P.Product'NTuple Tuple where - fromProto r = do - fs <- traverse fromProto $ r ^. P.fields - si <- fromProto $ r ^. P.sourceInfo - pure $ Tuple fs si - - toProto (Tuple fs si) = - defMessage - & P.fields .~ (toProto <$> fs) - & P.sourceInfo .~ toProto si - -instance IsMessage P.Product Product where - fromProto p = case p ^. P.maybe'product of - Nothing -> throwOneOfError (messageName (Proxy @P.Product)) "product" - Just x -> case x of - --- wrong, fix - P.Product'Record' r -> do - recrd <- fromProto r - pure $ RecordI recrd - P.Product'Ntuple t -> do - tup <- fromProto t - pure $ TupleI tup - - toProto = \case - RecordI r -> defMessage & P.record .~ toProto r - TupleI t -> defMessage & P.ntuple .~ toProto t - -instance IsMessage P.Product'Record'Field Field where - fromProto f = do - fnm <- fromProto $ f ^. P.fieldName - fty <- fromProto $ f ^. P.fieldTy - pure $ Field fnm fty - - toProto (Field fnm fty) = - defMessage - & P.fieldName .~ toProto fnm - & P.fieldTy .~ toProto fty - -{- - Classes, instances, constraints --} - -instance IsMessage P.TyClassRef'Local LocalClassRef where - fromProto lr = do - si <- fromProto $ lr ^. P.sourceInfo - nm <- fromProto $ lr ^. P.className - pure $ LocalClassRef nm si - - toProto (LocalClassRef nm si) = - defMessage - & P.className .~ toProto nm - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyClassRef'Foreign ForeignClassRef where - fromProto fr = do - si <- fromProto $ fr ^. P.sourceInfo - mn <- fromProto $ fr ^. P.moduleName - tn <- fromProto $ fr ^. P.className - pure $ ForeignClassRef tn mn si - - toProto (ForeignClassRef tn mn si) = - defMessage - & P.className .~ toProto tn - & P.moduleName .~ toProto mn - & P.sourceInfo .~ toProto si - -instance IsMessage P.TyClassRef TyClassRef where - fromProto tr = case tr ^. P.maybe'classRef of - Nothing -> throwOneOfError (messageName (Proxy @P.TyClassRef)) "class_ref" - Just x -> case x of - P.TyClassRef'LocalClassRef lr -> LocalCI <$> fromProto lr - P.TyClassRef'ForeignClassRef f -> ForeignCI <$> fromProto f - - toProto = \case - LocalCI lr -> defMessage & P.localClassRef .~ toProto lr - ForeignCI fr -> defMessage & P.foreignClassRef .~ toProto fr - -instance IsMessage P.ClassDef ClassDef where - fromProto cd = do - ctx <- ask - ctxMn <- case ctx of - CtxModule mn -> return mn - _ -> throwInternalError "Expected to be in Module Context" - local (const $ CtxClassDef ctxMn cd) $ do - si <- fromProto $ cd ^. P.sourceInfo - cnm <- fromProto $ cd ^. P.className - cargs <- traverse fromProto $ cd ^. P.classArgs - carg <- case cargs of - [] -> throwInternalError "Zero parameter type classes are not supported" - [x] -> return x - _ -> throwInternalError "Multi parameter type classes are not supported" - sups <- traverse fromProto $ cd ^. P.supers - let doc = cd ^. P.documentation - pure $ ClassDef cnm carg sups doc si - - toProto (ClassDef cnm carg sups doc si) = - defMessage - & P.className .~ toProto cnm - & P.classArgs .~ pure (toProto carg) - & P.supers .~ (toProto <$> sups) - & P.documentation .~ doc - & P.sourceInfo .~ toProto si - -instance IsMessage P.InstanceClause InstanceClause where - fromProto ic = do - si <- fromProto $ ic ^. P.sourceInfo - cnm <- fromProto $ ic ^. P.classRef - csts <- traverse fromProto $ ic ^. P.constraints - args <- traverse fromProto $ ic ^. P.args - arg <- case args of - [] -> throwInternalError "Zero instance arguments, but zero parameter type classes are not supported" - [x] -> return x - _ -> throwInternalError "Multiple instance arguments, but multi parameter type classes are not supported" - pure $ InstanceClause cnm arg csts si - - toProto (InstanceClause cnm hd csts si) = - defMessage - & P.classRef .~ toProto cnm - & P.args .~ pure (toProto hd) - & P.constraints .~ (toProto <$> csts) - & P.sourceInfo .~ toProto si - -instance IsMessage P.Constraint Constraint where - fromProto c = do - si <- fromProto $ c ^. P.sourceInfo - cnm <- fromProto $ c ^. P.classRef - args <- traverse fromProto $ c ^. P.arguments - arg <- case args of - [] -> throwInternalError "Zero constraint arguments, but zero parameter type classes are not supported" - [x] -> return x - _ -> throwInternalError "Multiple constraint arguments, but multi parameter type classes are not supported" - pure $ Constraint cnm arg si - - toProto (Constraint cnm arg si) = - defMessage - & P.classRef .~ toProto cnm - & P.arguments .~ pure (toProto arg) - & P.sourceInfo .~ toProto si - -{- - Module, CompilerInput --} - -parseAndIndex :: forall {t :: Type -> Type} {proto} {a} {k}. (Foldable t, IsMessage proto a, Ord k) => (a -> k) -> t proto -> FromProto (Map k a, Map k [proto]) -parseAndIndex key = - foldlM - ( \(indexed, multiples) px -> do - x <- fromProto px - let k = key x - if Map.member k indexed - then return (indexed, Map.insertWith (++) k [px] multiples) - else return (Map.insert k x indexed, multiples) - ) - (mempty, mempty) - -stripSourceInfo :: HasField "sourceInfo" s t a SourceInfo => s -> t -stripSourceInfo x = x & #sourceInfo .~ defSourceInfo - -instance IsMessage P.Module Module where - fromProto m = do - ctx <- ask - case ctx of - CtxCompilerInput -> return () - _ -> throwInternalError "Expected to be in CompilerInput Context" - local (const $ CtxModule (m ^. P.moduleName)) $ do - mnm <- fromProto $ m ^. P.moduleName - (tydefs, mulTyDefs) <- parseAndIndex (\tyDef -> stripSourceInfo $ tyDef ^. #tyName) (m ^. P.typeDefs) - (cldefs, mulClDefs) <- parseAndIndex (\cldef -> stripSourceInfo $ cldef ^. #className) (m ^. P.classDefs) - (impts, mulImpts) <- parseAndIndex stripSourceInfo (m ^. P.imports) - insts <- traverse fromProto $ m ^. P.instances - si <- fromProto $ m ^. P.sourceInfo - let mulTyDefsErrs = - [ ProtoParseError $ - defMessage - & P.multipleTydefError . P.moduleName .~ (m ^. P.moduleName) - & P.multipleTydefError . P.tyDefs .~ tds - | (_tn, tds) <- Map.toList mulTyDefs - ] - mulClassDefsErrs = - [ ProtoParseError $ - defMessage - & P.multipleClassdefError . P.moduleName .~ (m ^. P.moduleName) - & P.multipleClassdefError . P.classDefs .~ cds - | (_cn, cds) <- Map.toList mulClDefs - ] - mulImptsErrs = - [ ProtoParseError $ - defMessage - & P.multipleImportError . P.moduleName .~ (m ^. P.moduleName) - & P.multipleImportError . P.imports .~ ims - | (_in, ims) <- Map.toList mulImpts - ] - protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs ++ mulImptsErrs - if null protoParseErrs - then pure $ Module mnm tydefs cldefs insts (Map.keysSet impts) si - else throwError protoParseErrs - - toProto (Module mnm tdefs cdefs insts impts si) = - defMessage - & P.moduleName .~ toProto mnm - & P.typeDefs .~ (toProto <$> toList tdefs) - & P.classDefs .~ (toProto <$> toList cdefs) - & P.instances .~ (toProto <$> insts) - & P.imports .~ (toProto <$> Set.toList impts) - & P.sourceInfo .~ toProto si - -instance IsMessage P.CompilerInput CompilerInput where - fromProto ci = do - local (const CtxCompilerInput) $ do - (mods, mulModules) <- parseAndIndex (\m -> stripSourceInfo $ m ^. #moduleName) (ci ^. P.modules) - let mulModulesErrs = - [ ProtoParseError $ - defMessage & P.multipleModuleError . P.modules .~ ms - | (_mn, ms) <- Map.toList mulModules - ] - if null mulModulesErrs - then pure $ CompilerInput mods - else throwError mulModulesErrs - - toProto (CompilerInput ms) = - defMessage - & P.modules .~ (toProto <$> toList ms) - -{- - Outputs --} - -instance IsMessage P.KindCheckError KindCheckError where - fromProto kce = - case kce ^. P.maybe'kindCheckError of - Just x -> case x of - P.KindCheckError'UnboundTermError' err -> - UnboundTermError - <$> fromProto (err ^. P.tyName) - <*> fromProto (err ^. P.varName) - P.KindCheckError'UnificationError err -> - IncorrectApplicationError - <$> fromProto (err ^. P.tyName) - <*> fromProto (err ^. P.tyKind1) - <*> fromProto (err ^. P.tyKind2) - P.KindCheckError'RecursiveSubsError err -> - RecursiveKindError - <$> fromProto (err ^. P.tyName) - P.KindCheckError'InconsistentTypeError' err -> - InconsistentTypeError - <$> fromProto (err ^. P.tyName) - <*> fromProto (err ^. P.inferredKind) - <*> fromProto (err ^. P.definedKind) - Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckError)) "kind_check_error" - - toProto = \case - UnboundTermError tyname varname -> - defMessage - & (P.unboundTermError . P.tyName) .~ toProto tyname - & (P.unboundTermError . P.varName) .~ toProto varname - IncorrectApplicationError name k1 k2 -> - defMessage - & (P.unificationError . P.tyName) .~ toProto name - & (P.unificationError . P.tyKind1) .~ toProto k1 - & (P.unificationError . P.tyKind2) .~ toProto k2 - RecursiveKindError err -> - defMessage - & (P.recursiveSubsError . P.tyName) .~ toProto err - InconsistentTypeError name ki kd -> - defMessage - & (P.inconsistentTypeError . P.tyName) .~ toProto name - & (P.inconsistentTypeError . P.inferredKind) .~ toProto ki - & (P.inconsistentTypeError . P.definedKind) .~ toProto kd - --- instance IsMessage P.CompilerError CompilerError where --- fromProto cErr = case cErr ^. P.maybe'compilerError of --- Just x -> case x of --- P.CompilerError'KindCheckError err -> CompKindCheckError <$> fromProto err --- P.CompilerError'InternalError err -> InternalError <$> fromProto (err ^. P.internalError) --- Nothing -> throwProtoError EmptyField - --- toProto = \case --- CompKindCheckError err -> defMessage & P.kindCheckError .~ toProto err --- InternalError err -> defMessage & (P.internalError . P.internalError) .~ toProto err - --- instance IsMessage P.CompilerResult CompilerResult where --- fromProto c = --- if c == defMessage --- then pure CompilerResult --- else throwProtoError EmptyField --- toProto CompilerResult = defMessage - --- instance IsMessage P.CompilerOutput CompilerOutput where --- fromProto co = case co ^. P.maybe'compilerOutput of --- Just (P.CompilerOutput'CompilerResult res) -> Right <$> fromProto res --- Just (P.CompilerOutput'CompilerError err) -> Left <$> fromProto err --- Nothing -> throwProtoError EmptyField - --- toProto = \case --- Right res -> defMessage & P.compilerResult .~ toProto res --- Left err -> defMessage & P.compilerError .~ toProto err - --- | Convert from internal Kind to Proto Kind. -kind2ProtoKind :: K.Kind -> Kind -kind2ProtoKind = \case - k1 K.:->: k2 -> Kind $ KindArrow (kind2ProtoKind k1) (kind2ProtoKind k2) - K.Type -> Kind . KindRef $ KType - K.KVar _ -> Kind . KindRef $ KUnspecified -- this shouldn't happen. - --- | Convert from internal Kind to Proto Kind. -protoKind2Kind :: Kind -> K.Kind -protoKind2Kind = \case - Kind k -> case k of - KindArrow k1 k2 -> protoKind2Kind k1 K.:->: protoKind2Kind k2 - KindRef KType -> K.Type - KindRef KUnspecified -> K.KVar "Unspecified" +import LambdaBuffers.Compiler.ProtoCompat.FromProto as FromProto +import LambdaBuffers.Compiler.ProtoCompat.Types as Types diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs new file mode 100644 index 00000000..dde057f7 --- /dev/null +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -0,0 +1,738 @@ +module LambdaBuffers.Compiler.ProtoCompat.FromProto ( + IsMessage (..), + FromProtoErr (..), + protoKind2Kind, + kind2ProtoKind, + runFromProto, +) where + +import Control.Lens ((&), (.~), (^.)) +import Control.Monad.Except (Except, MonadError (throwError), runExcept) +import Control.Monad.Reader (MonadReader (ask, local), ReaderT (runReaderT)) +import Data.Foldable (foldlM, toList) +import Data.Generics.Labels () +import Data.Generics.Product (HasField) +import Data.Kind (Type) +import Data.Map (Map) +import Data.Map qualified as Map +import Data.ProtoLens (Message (messageName), MessageEnum (showEnum), defMessage) +import Data.Proxy (Proxy (Proxy)) +import Data.Set qualified as Set +import Data.Text (Text) +import Data.Text qualified as Text +import GHC.Generics (Generic) +import LambdaBuffers.Compiler.KindCheck.Kind qualified as K +import LambdaBuffers.Compiler.NamingCheck (checkClassName, checkConstrName, checkFieldName, checkModuleNamePart, checkTyName, checkVarName) +import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC +import Proto.Compiler (NamingError) +import Proto.Compiler qualified as P +import Proto.Compiler_Fields qualified as P + +data FromProtoErr + = FPNamingError P.NamingError + | FPInternalError P.InternalError + | FPProtoParseError P.ProtoParseError + deriving stock (Show, Eq, Ord, Generic) + +data FromProtoContext + = CtxCompilerInput + | CtxModule P.ModuleName + | CtxTyDef P.ModuleName P.TyDef + | CtxClassDef P.ModuleName P.ClassDef + deriving stock (Show, Eq, Ord, Generic) + +type FromProto a = ReaderT FromProtoContext (Except [FromProtoErr]) a + +-- | Parse a Proto API CompilerInput into the internal CompilerInput representation or report errors. +runFromProto :: P.CompilerInput -> Either [FromProtoErr] PC.CompilerInput +runFromProto compInp = do + let exM = runReaderT (fromProto compInp) CtxCompilerInput + runExcept exM + +class IsMessage (proto :: Type) (good :: Type) where + fromProto :: proto -> FromProto good + + toProto :: good -> proto + +throwNamingError :: Either NamingError b -> FromProto b +throwNamingError = either (\err -> throwError [FPNamingError err]) return + +throwOneOfError :: Text -> Text -> FromProto b +throwOneOfError protoMsgName protoFieldName = + throwError + [ FPProtoParseError $ + defMessage + & P.oneOfNotSetError . P.messageName .~ protoMsgName + & P.oneOfNotSetError . P.fieldName .~ protoFieldName + ] + +throwInternalError :: Text -> FromProto b +throwInternalError msg = throwError [FPInternalError $ defMessage & P.msg .~ msg] + +parseAndIndex :: forall {t :: Type -> Type} {proto} {a} {k}. (Foldable t, IsMessage proto a, Ord k) => (a -> k) -> t proto -> FromProto (Map k a, Map k [proto]) +parseAndIndex key = + foldlM + ( \(indexed, multiples) px -> do + x <- fromProto px + let k = key x + if Map.member k indexed + then return (indexed, Map.insertWith (++) k [px] multiples) + else return (Map.insert k x indexed, multiples) + ) + (mempty, mempty) + +stripSourceInfo :: HasField "sourceInfo" s t a PC.SourceInfo => s -> t +stripSourceInfo x = x & #sourceInfo .~ PC.defSourceInfo + +{- + SourceInfo +-} + +instance IsMessage P.SourcePosition PC.SourcePosition where + fromProto sp = do + let col = fromIntegral $ sp ^. P.column + row = fromIntegral $ sp ^. P.row + pure $ PC.SourcePosition col row + + toProto sp = + defMessage + & P.column .~ fromIntegral (sp ^. #column) + & P.row .~ fromIntegral (sp ^. #row) + +instance IsMessage P.SourceInfo PC.SourceInfo where + fromProto si = do + let file = si ^. P.file + pFrom <- fromProto $ si ^. P.posFrom + pTo <- fromProto $ si ^. P.posTo + pure $ PC.SourceInfo file pFrom pTo + + toProto si = + defMessage + & P.file .~ (si ^. #file) + & P.posFrom .~ toProto (si ^. #posFrom) + & P.posTo .~ toProto (si ^. #posTo) + +{- + Names +-} + +instance IsMessage Text Text where + fromProto = pure + toProto = id + +instance IsMessage P.ModuleNamePart PC.ModuleNamePart where + fromProto mnp = do + si <- fromProto $ mnp ^. P.sourceInfo + throwNamingError $ checkModuleNamePart mnp + pure $ PC.ModuleNamePart (mnp ^. P.name) si + + toProto (PC.ModuleNamePart nm si) = + defMessage + & P.name .~ nm + & P.sourceInfo .~ toProto si + +instance IsMessage P.ModuleName PC.ModuleName where + fromProto mn = do + si <- fromProto $ mn ^. P.sourceInfo + parts <- traverse fromProto $ mn ^. P.parts + pure $ PC.ModuleName parts si + + toProto (PC.ModuleName parts si) = + defMessage + & P.parts .~ (toProto <$> parts) + & P.sourceInfo .~ toProto si + +instance IsMessage P.FieldName PC.FieldName where + fromProto v = do + throwNamingError $ checkFieldName v + PC.FieldName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) + + toProto (PC.FieldName n si) = + defMessage + & P.name .~ toProto n + & P.sourceInfo .~ toProto si + +instance IsMessage P.ConstrName PC.ConstrName where + fromProto v = do + throwNamingError $ checkConstrName v + PC.ConstrName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) + + toProto (PC.ConstrName n si) = + defMessage + & P.name .~ toProto n + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyName PC.TyName where + fromProto v = do + throwNamingError $ checkTyName v + PC.TyName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) + + toProto (PC.TyName n si) = + defMessage + & P.name .~ toProto n + & P.sourceInfo .~ toProto si + +instance IsMessage P.ClassName PC.ClassName where + fromProto v = do + throwNamingError $ checkClassName v + PC.ClassName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) + + toProto (PC.ClassName n si) = + defMessage + & P.name .~ toProto n + & P.sourceInfo .~ toProto si + +instance IsMessage P.VarName PC.VarName where + fromProto v = do + throwNamingError $ checkVarName v + PC.VarName <$> fromProto (v ^. P.name) <*> fromProto (v ^. P.sourceInfo) + + toProto (PC.VarName n si) = + defMessage + & P.name .~ toProto n + & P.sourceInfo .~ toProto si + +{- + Ty & Components +-} + +instance IsMessage P.TyVar PC.TyVar where + fromProto tv = do + vn <- fromProto $ tv ^. P.varName + si <- fromProto $ tv ^. P.sourceInfo + pure $ PC.TyVar vn si + + toProto (PC.TyVar vn si) = + defMessage + & P.varName .~ toProto vn + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyApp PC.TyApp where + fromProto ta = do + tf <- fromProto $ ta ^. P.tyFunc + si <- fromProto $ ta ^. P.sourceInfo + targs <- traverse fromProto $ ta ^. P.tyArgs + pure $ PC.TyApp tf targs si + + toProto (PC.TyApp tf args si) = + defMessage + & P.tyFunc .~ toProto tf + & P.tyArgs .~ toList (toProto <$> args) + & P.sourceInfo .~ toProto si + +instance IsMessage P.Ty PC.Ty where + fromProto ti = case ti ^. P.maybe'ty of + Nothing -> throwOneOfError (messageName (Proxy @P.Ty)) "ty" + Just x -> case x of + P.Ty'TyVar tv -> PC.TyVarI <$> fromProto tv + P.Ty'TyApp ta -> PC.TyAppI <$> fromProto ta + P.Ty'TyRef tr -> PC.TyRefI <$> fromProto tr + + toProto = \case + PC.TyVarI tv -> defMessage & P.tyVar .~ toProto tv + PC.TyRefI tr -> defMessage & P.tyRef .~ toProto tr + PC.TyAppI ta -> defMessage & P.tyApp .~ toProto ta + +instance IsMessage P.TyRef'Local PC.LocalRef where + fromProto lr = do + si <- fromProto $ lr ^. P.sourceInfo + nm <- fromProto $ lr ^. P.tyName + pure $ PC.LocalRef nm si + + toProto (PC.LocalRef nm si) = + defMessage + & P.tyName .~ toProto nm + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyRef'Foreign PC.ForeignRef where + fromProto fr = do + si <- fromProto $ fr ^. P.sourceInfo + mn <- fromProto $ fr ^. P.moduleName + tn <- fromProto $ fr ^. P.tyName + pure $ PC.ForeignRef tn mn si + + toProto (PC.ForeignRef tn mn si) = + defMessage + & P.tyName .~ toProto tn + & P.moduleName .~ toProto mn + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyRef PC.TyRef where + fromProto tr = case tr ^. P.maybe'tyRef of + Nothing -> throwOneOfError (messageName (Proxy @P.TyRef)) "ty_ref" + Just x -> case x of + P.TyRef'LocalTyRef lr -> PC.LocalI <$> fromProto lr + P.TyRef'ForeignTyRef f -> PC.ForeignI <$> fromProto f + + toProto = \case + PC.LocalI lr -> defMessage & P.localTyRef .~ toProto lr + PC.ForeignI fr -> defMessage & P.foreignTyRef .~ toProto fr + +{- + TyDef & Components +-} + +instance IsMessage P.TyDef PC.TyDef where + fromProto td = do + ctx <- ask + ctxModuleName <- case ctx of + CtxModule mn -> return mn + _ -> throwInternalError "Expected to be in Module Context" + local (const $ CtxTyDef ctxModuleName td) $ do + tnm <- fromProto $ td ^. P.tyName + tyabs <- fromProto $ td ^. P.tyAbs + si <- fromProto $ td ^. P.sourceInfo + pure $ PC.TyDef tnm tyabs si + + toProto (PC.TyDef tnm tyabs si) = + defMessage + & P.tyName .~ toProto tnm + & P.tyAbs .~ toProto tyabs + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyAbs PC.TyAbs where + fromProto ta = do + (tyargs, mulTyArgs) <- parseAndIndex (\a -> stripSourceInfo $ a ^. #argName) (ta ^. P.tyArgs) + tybody <- fromProto $ ta ^. P.tyBody + si <- fromProto $ ta ^. P.sourceInfo + ctx <- ask + (ctxMn, ctxTyd) <- case ctx of + CtxTyDef mn tyd -> return (mn, tyd) + _ -> throwInternalError "Expected to be in TyDef Context" + let mulArgsErrs = + [ FPProtoParseError $ + defMessage + & P.multipleTyargError . P.moduleName .~ ctxMn + & P.multipleTyargError . P.tyDef .~ ctxTyd + & P.multipleTyargError . P.tyArgs .~ args + | (_an, args) <- Map.toList mulTyArgs + ] + if null mulArgsErrs + then pure $ PC.TyAbs tyargs tybody si + else throwError mulArgsErrs + + toProto (PC.TyAbs tyargs tyabs si) = + defMessage + & P.tyArgs .~ (toProto <$> toList tyargs) + & P.tyBody .~ toProto tyabs + & P.sourceInfo .~ toProto si + +instance IsMessage P.Kind'KindRef PC.KindRefType where + fromProto kr = + ( \case + P.Kind'KIND_REF_TYPE -> pure PC.KType + P.Kind'KIND_REF_UNSPECIFIED -> pure PC.KUnspecified + P.Kind'KindRef'Unrecognized v -> + throwError + [ FPProtoParseError $ + defMessage + & P.unknownEnumError . P.enumName .~ Text.pack (showEnum kr) + & P.unknownEnumError . P.gotTag .~ (Text.pack . show $ v) + ] + ) + kr + + toProto = \case + PC.KType -> P.Kind'KIND_REF_TYPE + PC.KUnspecified -> P.Kind'KIND_REF_UNSPECIFIED + +instance IsMessage P.Kind PC.Kind where + fromProto k = do + kt <- case k ^. P.maybe'kind of + Nothing -> throwOneOfError (messageName (Proxy @P.Kind)) "kind" + Just k' -> case k' of + P.Kind'KindRef r -> PC.KindRef <$> fromProto r + P.Kind'KindArrow' arr -> PC.KindArrow <$> fromProto (arr ^. P.left) <*> fromProto (arr ^. P.right) + pure $ PC.Kind kt + + toProto (PC.Kind (PC.KindArrow l r)) = do + defMessage + & P.kindArrow . P.left .~ toProto l + & P.kindArrow . P.right .~ toProto r + toProto (PC.Kind (PC.KindRef r)) = do + defMessage + & P.kindRef .~ toProto r + +instance IsMessage P.TyArg PC.TyArg where + fromProto ta = do + argnm <- fromProto $ ta ^. P.argName + si <- fromProto $ ta ^. P.sourceInfo + kind <- fromProto $ ta ^. P.argKind + pure $ PC.TyArg argnm kind si + + toProto (PC.TyArg argnm argkind si) = + defMessage + & P.argName .~ toProto argnm + & P.argKind .~ toProto argkind + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyBody PC.TyBody where + fromProto tb = case tb ^. P.maybe'tyBody of + Nothing -> throwOneOfError (messageName (Proxy @P.TyBody)) "ty_body" + Just x -> case x of + P.TyBody'Opaque opq -> PC.OpaqueI <$> fromProto (opq ^. P.sourceInfo) + P.TyBody'Sum sumI -> PC.SumI <$> fromProto sumI + + toProto = \case + PC.OpaqueI si -> + let opaque = defMessage & P.sourceInfo .~ toProto si + in defMessage & P.opaque .~ opaque + PC.SumI sb -> defMessage & P.sum .~ toProto sb + +instance IsMessage P.Sum PC.Sum where + fromProto s = do + (ctors, mulCtors) <- parseAndIndex (\c -> stripSourceInfo $ c ^. #constrName) (s ^. P.constructors) + si <- fromProto $ s ^. P.sourceInfo + ctx <- ask + (ctxMn, ctxTyd) <- case ctx of + CtxTyDef mn tyd -> return (mn, tyd) + _ -> throwInternalError "Expected to be in TyDef Context" + let mulCtorsErrs = + [ FPProtoParseError $ + defMessage + & P.multipleConstructorError . P.moduleName .~ ctxMn + & P.multipleConstructorError . P.tyDef .~ ctxTyd + & P.multipleConstructorError . P.constructors .~ cs + | (_cn, cs) <- Map.toList mulCtors + ] + if null mulCtorsErrs + then pure $ PC.Sum ctors si + else throwError mulCtorsErrs + + toProto (PC.Sum ctors si) = + defMessage + & P.constructors .~ toList (toProto <$> ctors) + & P.sourceInfo .~ toProto si + +instance IsMessage P.Sum'Constructor PC.Constructor where + fromProto c = do + cnm <- fromProto $ c ^. P.constrName + prod <- fromProto $ c ^. P.product + pure $ PC.Constructor cnm prod + + toProto (PC.Constructor cnm prod) = + defMessage + & P.constrName .~ toProto cnm + & P.product .~ toProto prod + +instance IsMessage P.Product'Record PC.Record where + fromProto r = do + (fields, mulFields) <- parseAndIndex (\f -> stripSourceInfo $ f ^. #fieldName) (r ^. P.fields) + si <- fromProto $ r ^. P.sourceInfo + ctx <- ask + (ctxMn, ctxTyd) <- case ctx of + CtxTyDef mn tyd -> return (mn, tyd) + _ -> throwInternalError "Expected to be in TyDef Context" + let mulFieldsErrs = + [ FPProtoParseError $ + defMessage + & P.multipleFieldError . P.moduleName .~ ctxMn + & P.multipleFieldError . P.tyDef .~ ctxTyd + & P.multipleFieldError . P.fields .~ fs + | (_fn, fs) <- Map.toList mulFields + ] + if null mulFieldsErrs + then pure $ PC.Record fields si + else throwError mulFieldsErrs + + toProto (PC.Record fs si) = + defMessage + & P.fields .~ (toProto <$> toList fs) + & P.sourceInfo .~ toProto si + +instance IsMessage P.Product'NTuple PC.Tuple where + fromProto r = do + fs <- traverse fromProto $ r ^. P.fields + si <- fromProto $ r ^. P.sourceInfo + pure $ PC.Tuple fs si + + toProto (PC.Tuple fs si) = + defMessage + & P.fields .~ (toProto <$> fs) + & P.sourceInfo .~ toProto si + +instance IsMessage P.Product PC.Product where + fromProto p = case p ^. P.maybe'product of + Nothing -> throwOneOfError (messageName (Proxy @P.Product)) "product" + Just x -> case x of + --- wrong, fix + P.Product'Record' r -> do + recrd <- fromProto r + pure $ PC.RecordI recrd + P.Product'Ntuple t -> do + tup <- fromProto t + pure $ PC.TupleI tup + + toProto = \case + PC.RecordI r -> defMessage & P.record .~ toProto r + PC.TupleI t -> defMessage & P.ntuple .~ toProto t + +instance IsMessage P.Product'Record'Field PC.Field where + fromProto f = do + fnm <- fromProto $ f ^. P.fieldName + fty <- fromProto $ f ^. P.fieldTy + pure $ PC.Field fnm fty + + toProto (PC.Field fnm fty) = + defMessage + & P.fieldName .~ toProto fnm + & P.fieldTy .~ toProto fty + +{- + Classes, instances, constraints +-} + +instance IsMessage P.TyClassRef'Local PC.LocalClassRef where + fromProto lr = do + si <- fromProto $ lr ^. P.sourceInfo + nm <- fromProto $ lr ^. P.className + pure $ PC.LocalClassRef nm si + + toProto (PC.LocalClassRef nm si) = + defMessage + & P.className .~ toProto nm + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyClassRef'Foreign PC.ForeignClassRef where + fromProto fr = do + si <- fromProto $ fr ^. P.sourceInfo + mn <- fromProto $ fr ^. P.moduleName + tn <- fromProto $ fr ^. P.className + pure $ PC.ForeignClassRef tn mn si + + toProto (PC.ForeignClassRef tn mn si) = + defMessage + & P.className .~ toProto tn + & P.moduleName .~ toProto mn + & P.sourceInfo .~ toProto si + +instance IsMessage P.TyClassRef PC.TyClassRef where + fromProto tr = case tr ^. P.maybe'classRef of + Nothing -> throwOneOfError (messageName (Proxy @P.TyClassRef)) "class_ref" + Just x -> case x of + P.TyClassRef'LocalClassRef lr -> PC.LocalCI <$> fromProto lr + P.TyClassRef'ForeignClassRef f -> PC.ForeignCI <$> fromProto f + + toProto = \case + PC.LocalCI lr -> defMessage & P.localClassRef .~ toProto lr + PC.ForeignCI fr -> defMessage & P.foreignClassRef .~ toProto fr + +instance IsMessage P.ClassDef PC.ClassDef where + fromProto cd = do + ctx <- ask + ctxMn <- case ctx of + CtxModule mn -> return mn + _ -> throwInternalError "Expected to be in Module Context" + local (const $ CtxClassDef ctxMn cd) $ do + si <- fromProto $ cd ^. P.sourceInfo + cnm <- fromProto $ cd ^. P.className + cargs <- traverse fromProto $ cd ^. P.classArgs + carg <- case cargs of + [] -> throwInternalError "Zero parameter type classes are not supported" + [x] -> return x + _ -> throwInternalError "Multi parameter type classes are not supported" + sups <- traverse fromProto $ cd ^. P.supers + let doc = cd ^. P.documentation + pure $ PC.ClassDef cnm carg sups doc si + + toProto (PC.ClassDef cnm carg sups doc si) = + defMessage + & P.className .~ toProto cnm + & P.classArgs .~ pure (toProto carg) + & P.supers .~ (toProto <$> sups) + & P.documentation .~ doc + & P.sourceInfo .~ toProto si + +instance IsMessage P.InstanceClause PC.InstanceClause where + fromProto ic = do + si <- fromProto $ ic ^. P.sourceInfo + cnm <- fromProto $ ic ^. P.classRef + csts <- traverse fromProto $ ic ^. P.constraints + args <- traverse fromProto $ ic ^. P.args + arg <- case args of + [] -> throwInternalError "Zero instance arguments, but zero parameter type classes are not supported" + [x] -> return x + _ -> throwInternalError "Multiple instance arguments, but multi parameter type classes are not supported" + pure $ PC.InstanceClause cnm arg csts si + + toProto (PC.InstanceClause cnm hd csts si) = + defMessage + & P.classRef .~ toProto cnm + & P.args .~ pure (toProto hd) + & P.constraints .~ (toProto <$> csts) + & P.sourceInfo .~ toProto si + +instance IsMessage P.Constraint PC.Constraint where + fromProto c = do + si <- fromProto $ c ^. P.sourceInfo + cnm <- fromProto $ c ^. P.classRef + args <- traverse fromProto $ c ^. P.arguments + arg <- case args of + [] -> throwInternalError "Zero constraint arguments, but zero parameter type classes are not supported" + [x] -> return x + _ -> throwInternalError "Multiple constraint arguments, but multi parameter type classes are not supported" + pure $ PC.Constraint cnm arg si + + toProto (PC.Constraint cnm arg si) = + defMessage + & P.classRef .~ toProto cnm + & P.arguments .~ pure (toProto arg) + & P.sourceInfo .~ toProto si + +{- + Module, CompilerInput +-} + +instance IsMessage P.Module PC.Module where + fromProto m = do + ctx <- ask + case ctx of + CtxCompilerInput -> return () + _ -> throwInternalError "Expected to be in CompilerInput Context" + local (const $ CtxModule (m ^. P.moduleName)) $ do + mnm <- fromProto $ m ^. P.moduleName + (tydefs, mulTyDefs) <- parseAndIndex (\tyDef -> stripSourceInfo $ tyDef ^. #tyName) (m ^. P.typeDefs) + (cldefs, mulClDefs) <- parseAndIndex (\cldef -> stripSourceInfo $ cldef ^. #className) (m ^. P.classDefs) + (impts, mulImpts) <- parseAndIndex stripSourceInfo (m ^. P.imports) + insts <- traverse fromProto $ m ^. P.instances + si <- fromProto $ m ^. P.sourceInfo + let mulTyDefsErrs = + [ FPProtoParseError $ + defMessage + & P.multipleTydefError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleTydefError . P.tyDefs .~ tds + | (_tn, tds) <- Map.toList mulTyDefs + ] + mulClassDefsErrs = + [ FPProtoParseError $ + defMessage + & P.multipleClassdefError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleClassdefError . P.classDefs .~ cds + | (_cn, cds) <- Map.toList mulClDefs + ] + mulImptsErrs = + [ FPProtoParseError $ + defMessage + & P.multipleImportError . P.moduleName .~ (m ^. P.moduleName) + & P.multipleImportError . P.imports .~ ims + | (_in, ims) <- Map.toList mulImpts + ] + protoParseErrs = mulTyDefsErrs ++ mulClassDefsErrs ++ mulImptsErrs + if null protoParseErrs + then pure $ PC.Module mnm tydefs cldefs insts (Map.keysSet impts) si + else throwError protoParseErrs + + toProto (PC.Module mnm tdefs cdefs insts impts si) = + defMessage + & P.moduleName .~ toProto mnm + & P.typeDefs .~ (toProto <$> toList tdefs) + & P.classDefs .~ (toProto <$> toList cdefs) + & P.instances .~ (toProto <$> insts) + & P.imports .~ (toProto <$> Set.toList impts) + & P.sourceInfo .~ toProto si + +instance IsMessage P.CompilerInput PC.CompilerInput where + fromProto ci = do + local (const CtxCompilerInput) $ do + (mods, mulModules) <- parseAndIndex (\m -> stripSourceInfo $ m ^. #moduleName) (ci ^. P.modules) + let mulModulesErrs = + [ FPProtoParseError $ + defMessage & P.multipleModuleError . P.modules .~ ms + | (_mn, ms) <- Map.toList mulModules + ] + if null mulModulesErrs + then pure $ PC.CompilerInput mods + else throwError mulModulesErrs + + toProto (PC.CompilerInput ms) = + defMessage + & P.modules .~ (toProto <$> toList ms) + +{- + Outputs +-} + +instance IsMessage P.KindCheckError PC.KindCheckError where + fromProto kce = + case kce ^. P.maybe'kindCheckError of + Just x -> case x of + P.KindCheckError'UnboundTermError' err -> + PC.UnboundTermError + <$> fromProto (err ^. P.tyName) + <*> fromProto (err ^. P.varName) + P.KindCheckError'UnificationError err -> + PC.IncorrectApplicationError + <$> fromProto (err ^. P.tyName) + <*> fromProto (err ^. P.tyKind1) + <*> fromProto (err ^. P.tyKind2) + P.KindCheckError'RecursiveSubsError err -> + PC.RecursiveKindError + <$> fromProto (err ^. P.tyName) + P.KindCheckError'InconsistentTypeError' err -> + PC.InconsistentTypeError + <$> fromProto (err ^. P.tyName) + <*> fromProto (err ^. P.inferredKind) + <*> fromProto (err ^. P.definedKind) + Nothing -> throwOneOfError (messageName (Proxy @P.KindCheckError)) "kind_check_error" + + toProto = \case + PC.UnboundTermError tyname varname -> + defMessage + & (P.unboundTermError . P.tyName) .~ toProto tyname + & (P.unboundTermError . P.varName) .~ toProto varname + PC.IncorrectApplicationError name k1 k2 -> + defMessage + & (P.unificationError . P.tyName) .~ toProto name + & (P.unificationError . P.tyKind1) .~ toProto k1 + & (P.unificationError . P.tyKind2) .~ toProto k2 + PC.RecursiveKindError err -> + defMessage + & (P.recursiveSubsError . P.tyName) .~ toProto err + PC.InconsistentTypeError name ki kd -> + defMessage + & (P.inconsistentTypeError . P.tyName) .~ toProto name + & (P.inconsistentTypeError . P.inferredKind) .~ toProto ki + & (P.inconsistentTypeError . P.definedKind) .~ toProto kd + +-- instance IsMessage P.CompilerError CompilerError where +-- fromProto cErr = case cErr ^. P.maybe'compilerError of +-- Just x -> case x of +-- P.CompilerError'KindCheckError err -> CompKindCheckError <$> fromProto err +-- P.CompilerError'InternalError err -> InternalError <$> fromProto (err ^. P.internalError) +-- Nothing -> throwProtoError EmptyField + +-- toProto = \case +-- CompKindCheckError err -> defMessage & P.kindCheckError .~ toProto err +-- InternalError err -> defMessage & (P.internalError . P.internalError) .~ toProto err + +-- instance IsMessage P.CompilerResult CompilerResult where +-- fromProto c = +-- if c == defMessage +-- then pure CompilerResult +-- else throwProtoError EmptyField +-- toProto CompilerResult = defMessage + +-- instance IsMessage P.CompilerOutput CompilerOutput where +-- fromProto co = case co ^. P.maybe'compilerOutput of +-- Just (P.CompilerOutput'CompilerResult res) -> Right <$> fromProto res +-- Just (P.CompilerOutput'CompilerError err) -> Left <$> fromProto err +-- Nothing -> throwProtoError EmptyField + +-- toProto = \case +-- Right res -> defMessage & P.compilerResult .~ toProto res +-- Left err -> defMessage & P.compilerError .~ toProto err + +-- | Convert from internal Kind to Proto Kind. +kind2ProtoKind :: K.Kind -> PC.Kind +kind2ProtoKind = \case + k1 K.:->: k2 -> PC.Kind $ PC.KindArrow (kind2ProtoKind k1) (kind2ProtoKind k2) + K.Type -> PC.Kind . PC.KindRef $ PC.KType + K.KVar _ -> PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen. + +-- | Convert from internal Kind to Proto Kind. +protoKind2Kind :: PC.Kind -> K.Kind +protoKind2Kind = \case + PC.Kind k -> case k of + PC.KindArrow k1 k2 -> protoKind2Kind k1 K.:->: protoKind2Kind k2 + PC.KindRef PC.KType -> K.Type + PC.KindRef PC.KUnspecified -> K.KVar "Unspecified" From 58065fd5739a868c5d0f6e2a4814da54300445b0 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 13:07:08 +0100 Subject: [PATCH 10/20] Fixed the Cli --- .../app/LambdaBuffers/Compiler/Cli/Compile.hs | 42 ++++++------ .../src/LambdaBuffers/Compiler/KindCheck.hs | 2 +- .../Compiler/ProtoCompat/FromProto.hs | 64 +++++++++---------- 3 files changed, 56 insertions(+), 52 deletions(-) diff --git a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs index 576ef862..9ddca8c0 100644 --- a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs +++ b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs @@ -1,19 +1,17 @@ module LambdaBuffers.Compiler.Cli.Compile (CompileOpts (..), compile) where -import Control.Lens (makeLenses) +import Control.Lens (makeLenses, (&), (.~)) import Control.Lens.Getter ((^.)) import Data.ByteString qualified as BS +import Data.ProtoLens (Message (defMessage)) import Data.ProtoLens qualified as Pb import Data.ProtoLens.TextFormat qualified as PbText import Data.Text.Lazy qualified as Text import Data.Text.Lazy.IO qualified as Text -import LambdaBuffers.Compiler.KindCheck (check) -import LambdaBuffers.Compiler.ProtoCompat ( - FromProtoErr (NamingError, ProtoError), - IsMessage (fromProto, toProto), - ) -import LambdaBuffers.Compiler.ProtoCompat.Types qualified as ProtoCompat -import Proto.Compiler as ProtoLib (CompilerInput, CompilerOutput) +import LambdaBuffers.Compiler.KindCheck (check_) +import LambdaBuffers.Compiler.ProtoCompat (runFromProto, toProto) +import Proto.Compiler (CompilerError, CompilerInput, CompilerOutput) +import Proto.Compiler_Fields (compilerError, compilerResult) import System.FilePath.Lens (extension) data CompileOpts = CompileOpts @@ -24,20 +22,23 @@ data CompileOpts = CompileOpts makeLenses ''CompileOpts --- NOTE(cstml) - let's use Katip instead of print. +-- NOTE(cstml): Let's use Katip instead of print. -- | Compile LambdaBuffers modules compile :: CompileOpts -> IO () compile opts = do - compIn <- readCompilerInput (opts ^. input) - case fromProto @CompilerInput @ProtoCompat.CompilerInput compIn of - Left err -> case err of - NamingError ne -> print $ "Encountered a naming error " <> show ne - ProtoError pe -> print $ "Encountered a proto error " <> show pe - Right compIn' -> do - print @String "Successfully processed the CompilerInput" - let result = check compIn' - writeCompilerOutput (opts ^. output) (toProto result) + compInp <- readCompilerInput (opts ^. input) + case runFromProto compInp of + Left compErr -> do + print @String "Encountered errors during CompilerInput proto parsing" + writeCompilerError (opts ^. output) compErr + Right compInp' -> do + print @String "Successfully parsed the CompilerInput proto" + case check_ compInp' of + Left kcCompErr -> do + print @String "Encountered errors during CompilerInput proto parsing" + writeCompilerError (opts ^. output) (toProto kcCompErr) + Right _ -> writeCompilerOutput (opts ^. output) (defMessage & compilerResult .~ defMessage) return () readCompilerInput :: FilePath -> IO CompilerInput @@ -52,7 +53,10 @@ readCompilerInput fp = do return $ PbText.readMessageOrDie content _ -> error $ "Unknown CompilerInput format " <> ext -writeCompilerOutput :: FilePath -> ProtoLib.CompilerOutput -> IO () +writeCompilerError :: FilePath -> CompilerError -> IO () +writeCompilerError fp err = writeCompilerOutput fp (defMessage & compilerError .~ err) + +writeCompilerOutput :: FilePath -> CompilerOutput -> IO () writeCompilerOutput fp cr = do let ext = fp ^. extension case ext of diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index c2546819..55dec00a 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -77,7 +77,7 @@ data KindCheck a where InferTypeKind :: ModName -> P.TyDef -> Context -> Type -> KindCheck Kind CheckKindConsistency :: ModName -> P.TyDef -> Context -> Kind -> KindCheck Kind --- FIXME(cstml) add check for Context Consistency +-- FIXME(cstml): Add check for Context Consistency -- TyDefToTypes :: ModName -> P.TyDef -> KindCheck [Type] makeEffect ''KindCheck diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index dde057f7..a7938ef8 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -1,9 +1,8 @@ module LambdaBuffers.Compiler.ProtoCompat.FromProto ( - IsMessage (..), - FromProtoErr (..), protoKind2Kind, kind2ProtoKind, runFromProto, + toProto, ) where import Control.Lens ((&), (.~), (^.)) @@ -43,11 +42,22 @@ data FromProtoContext type FromProto a = ReaderT FromProtoContext (Except [FromProtoErr]) a --- | Parse a Proto API CompilerInput into the internal CompilerInput representation or report errors. -runFromProto :: P.CompilerInput -> Either [FromProtoErr] PC.CompilerInput +-- | Parse a Proto API CompilerInput into the internal CompilerInput representation or report errors (in Proto format). +runFromProto :: P.CompilerInput -> Either P.CompilerError PC.CompilerInput runFromProto compInp = do let exM = runReaderT (fromProto compInp) CtxCompilerInput - runExcept exM + errsOrRes = runExcept exM + case errsOrRes of + Left errs -> + let nerrs = [err | FPNamingError err <- errs] + pperrs = [err | FPProtoParseError err <- errs] + ierrs = [err | FPInternalError err <- errs] + in Left $ + defMessage + & P.namingErrors .~ nerrs + & P.protoParseErrors .~ pperrs + & P.internalErrors .~ ierrs + Right compIn' -> return compIn' class IsMessage (proto :: Type) (good :: Type) where fromProto :: proto -> FromProto good @@ -694,33 +704,23 @@ instance IsMessage P.KindCheckError PC.KindCheckError where & (P.inconsistentTypeError . P.inferredKind) .~ toProto ki & (P.inconsistentTypeError . P.definedKind) .~ toProto kd --- instance IsMessage P.CompilerError CompilerError where --- fromProto cErr = case cErr ^. P.maybe'compilerError of --- Just x -> case x of --- P.CompilerError'KindCheckError err -> CompKindCheckError <$> fromProto err --- P.CompilerError'InternalError err -> InternalError <$> fromProto (err ^. P.internalError) --- Nothing -> throwProtoError EmptyField - --- toProto = \case --- CompKindCheckError err -> defMessage & P.kindCheckError .~ toProto err --- InternalError err -> defMessage & (P.internalError . P.internalError) .~ toProto err - --- instance IsMessage P.CompilerResult CompilerResult where --- fromProto c = --- if c == defMessage --- then pure CompilerResult --- else throwProtoError EmptyField --- toProto CompilerResult = defMessage - --- instance IsMessage P.CompilerOutput CompilerOutput where --- fromProto co = case co ^. P.maybe'compilerOutput of --- Just (P.CompilerOutput'CompilerResult res) -> Right <$> fromProto res --- Just (P.CompilerOutput'CompilerError err) -> Left <$> fromProto err --- Nothing -> throwProtoError EmptyField - --- toProto = \case --- Right res -> defMessage & P.compilerResult .~ toProto res --- Left err -> defMessage & P.compilerError .~ toProto err +instance IsMessage P.CompilerError PC.CompilerError where + fromProto _ = throwInternalError "fromProto CompilerError not implemented" + + toProto = \case + PC.CompKindCheckError err -> defMessage & P.kindCheckErrors .~ [toProto err] + PC.InternalError err -> defMessage & P.internalErrors .~ [defMessage & P.msg .~ err] + +instance IsMessage P.CompilerResult PC.CompilerResult where + fromProto _ = throwInternalError "fromProto CompilerError not implemented" + toProto PC.CompilerResult = defMessage + +instance IsMessage P.CompilerOutput PC.CompilerOutput where + fromProto _ = throwInternalError "fromProto CompilerError not implemented" + + toProto = \case + Right res -> defMessage & P.compilerResult .~ toProto res + Left err -> defMessage & P.compilerError .~ toProto err -- | Convert from internal Kind to Proto Kind. kind2ProtoKind :: K.Kind -> PC.Kind From 22c4774b9ed891de911dda27b299686bea0b6079 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 16:00:52 +0100 Subject: [PATCH 11/20] Generators scaffold --- .../lambda-buffers-compiler.cabal | 6 +- lambda-buffers-compiler/test/Test.hs | 2 + .../test/Test/KindCheck.hs | 38 ++--- .../test/Test/LambdaBuffers/Compiler.hs | 6 + .../test/Test/LambdaBuffers/Compiler/Gen.hs | 132 ++++++++++++++++++ 5 files changed, 164 insertions(+), 20 deletions(-) create mode 100644 lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs create mode 100644 lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index 7837faa1..7c46932a 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -126,7 +126,7 @@ library hs-source-dirs: src --- note(cstml): should we name this something shorter? lb-cli? +-- NOTE(cstml): should we name this something shorter? lb-cli? executable lambda-buffers-compiler-cli import: common-language import: common-imports @@ -152,8 +152,10 @@ test-suite tests , containers >=0.6 , lambda-buffers-compiler , lambda-buffers-compiler-pb >=0.1 + , mtl >=2.2 , proto-lens >=0.7 , QuickCheck >=2.14 + , quickcheck-transformer , tasty >=1.4 , tasty-hunit >=0.10 , tasty-quickcheck >=0.10 @@ -161,6 +163,8 @@ test-suite tests other-modules: Test.KindCheck + Test.LambdaBuffers.Compiler + Test.LambdaBuffers.Compiler.Gen Test.TypeClassCheck Test.Utils.CompilerInput Test.Utils.Constructors diff --git a/lambda-buffers-compiler/test/Test.hs b/lambda-buffers-compiler/test/Test.hs index 936eb545..00770fcb 100644 --- a/lambda-buffers-compiler/test/Test.hs +++ b/lambda-buffers-compiler/test/Test.hs @@ -1,6 +1,7 @@ module Main (main) where import Test.KindCheck qualified as KC +import Test.LambdaBuffers.Compiler qualified as LBC import Test.Tasty (defaultMain, testGroup) import Test.TypeClassCheck qualified as TC @@ -11,4 +12,5 @@ main = "Compiler tests" [ KC.test , TC.test + , LBC.test ] diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index b4374912..7557bd12 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -22,7 +22,7 @@ import Test.QuickCheck ( (===), ) import Test.Tasty (TestTree, testGroup) -import Test.Tasty.HUnit (assertBool, testCase, (@?=)) +import Test.Tasty.HUnit (assertBool, assertEqual, testCase, (@?=)) import Test.Tasty.QuickCheck (testProperty) import Test.Utils.CompilerInput ( compilerInput'incoherent, @@ -44,18 +44,18 @@ testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe, kcTestFai trivialKCTest :: TestTree trivialKCTest = - testCase "Empty CompInput should check." $ + testCase "Empty CompInput should check" $ check_ (_CompilerInput []) @?= Right () kcTestMaybe :: TestTree kcTestMaybe = - testCase "Maybe should pass." $ + testCase "Maybe should pass" $ check_ compilerInput'maybe @?= Right () kcTestFailing :: TestTree kcTestFailing = - testCase "This should fail." $ - assertBool "Test should have failed." $ + testCase "This should fail" $ + assertBool "Test should have failed" $ check_ compilerInput'incoherent /= Right () {- | TyDef order does not matter when kind checking. @@ -67,9 +67,9 @@ kcTestFailing = -} kcTestOrdering :: TestTree kcTestOrdering = - testProperty "Module order inside the CompilerInput does not matter." $ - forAllShrink (resize 5 genModuleIn2Layouts) shrink $ - \(l, r) -> eitherFailOrPass (check_ l) == eitherFailOrPass (check_ r) + testProperty "Module order inside the CompilerInput does not matter" $ + forAllShrink (resize 2 genModuleIn2Layouts) shrink $ + \(l, r) -> check_ l === check_ r where genModuleIn2Layouts = do mods <- arbitrary @@ -86,8 +86,8 @@ testFolds :: TestTree testFolds = testGroup "Test Folds" - [ testGroup "Test Product Folds." [testFoldProd0, testFoldProd1, testFoldProd2, testFoldProd3, testPProdFoldTotal] - , testGroup "Test Sum Folds." [testSumFold0, testSumFold1, testSumFold2, testSumFold3] + [ testGroup "Test Product Folds" [testFoldProd0, testFoldProd1, testFoldProd2, testFoldProd3, testPProdFoldTotal] + , testGroup "Test Sum Folds" [testSumFold0, testSumFold1, testSumFold2, testSumFold3] ] prod :: Type -> Type -> Type @@ -99,32 +99,32 @@ unit' = Var tyUnit -- | [ ] -> unit testFoldProd0 :: TestTree testFoldProd0 = - testCase "Fold with product - 0 type." $ + testCase "Fold with product - 0 type" $ foldWithProduct [] @?= unit' -- | [ a ] -> prod unit a testFoldProd1 :: TestTree testFoldProd1 = - testCase "Fold with product - 1 type." $ + testCase "Fold with product - 1 type" $ foldWithProduct [lVar "a"] @?= prod unit' (lVar "a") -- | [b ,a] -> prod (prod unit b) a testFoldProd2 :: TestTree testFoldProd2 = - testCase "Fold with product - 2 types." $ + testCase "Fold with product - 2 types" $ foldWithProduct [lVar "b", lVar "a"] @?= prod (prod unit' (lVar "b")) (lVar "a") -- | [ a, b ,c ] -> prod (prod (prod unit c) b) a testFoldProd3 :: TestTree testFoldProd3 = - testCase "Fold with product - 2 types." $ + testCase "Fold with product - 2 types" $ foldWithProduct [lVar "c", lVar "b", lVar "a"] @?= prod (prod (prod unit' (lVar "c")) (lVar "b")) (lVar "a") testPProdFoldTotal :: TestTree testPProdFoldTotal = - testProperty "ProductFold is total." $ + testProperty "ProductFold is total" $ forAll arbitrary $ \ts -> foldWithProduct ts === foldWithProduct ts @@ -137,26 +137,26 @@ void' = Var tyVoid -- | [ ] -> void testSumFold0 :: TestTree testSumFold0 = - testCase "Fold 0 type." $ + testCase "Fold 0 type" $ foldWithSum [] @?= void' -- | [ a ] -> either void a testSumFold1 :: TestTree testSumFold1 = - testCase "Fold 1 type." $ + testCase "Fold 1 type" $ foldWithSum [lVar "a"] @?= either' void' (lVar "a") -- | [ a , b ] -> either (either void a) b testSumFold2 :: TestTree testSumFold2 = - testCase "Fold 2 type." $ + testCase "Fold 2 type" $ foldWithSum [lVar "b", lVar "a"] @?= either' (either' void' (lVar "b")) (lVar "a") -- | [ a , b , c ] -> a | ( b | c ) testSumFold3 :: TestTree testSumFold3 = - testCase "Fold 3 types." $ + testCase "Fold 3 types" $ foldWithSum [lVar "c", lVar "b", lVar "a"] @?= either' (either' (either' void' (lVar "c")) (lVar "b")) (lVar "a") diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs new file mode 100644 index 00000000..d091c619 --- /dev/null +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs @@ -0,0 +1,6 @@ +module Test.LambdaBuffers.Compiler (test) where + +import Test.Tasty (TestTree) + +test :: TestTree +test = undefined diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs new file mode 100644 index 00000000..de2ba463 --- /dev/null +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs @@ -0,0 +1,132 @@ +module Test.LambdaBuffers.Compiler.Gen (genCompilerInput) where + +import Control.Lens ((&), (.~), (^.)) +import Control.Monad.Reader (MonadTrans (lift), ReaderT, replicateM) +import Control.Monad.State (StateT) +import Data.List qualified as List +import Data.ProtoLens (Message (defMessage)) +import Data.Text (Text) +import Data.Text qualified as Text +import Data.Traversable (for) +import Proto.Compiler (ClassName, CompilerInput, ConstrName, Kind'KindRef (Kind'KIND_REF_TYPE), Module, ModuleName, ModuleNamePart, Sum, Sum'Constructor, Ty, TyAbs, TyArg, TyBody, TyDef, TyName, VarName) +import Proto.Compiler_Fields (argKind, argName, constrName, constructors, fields, kindRef, moduleName, modules, name, ntuple, parts, tyAbs, tyArgs, tyBody, tyName, tyVar, typeDefs, varName) +import Proto.Compiler_Fields qualified as P +import Test.QuickCheck qualified as QC (Gen, chooseEnum, chooseInt, elements, oneof, vectorOf) + +data GenProtoCtx +data GenProtoState + +type GenProto a = ReaderT GenProtoCtx (StateT GenProtoState QC.Gen) a + +vecOf :: forall {a}. GenProto a -> Int -> GenProto [a] +vecOf g n = replicateM n g + +chooseInt :: (Int, Int) -> GenProto Int +chooseInt r = lift . lift $ QC.chooseInt r + +-- | Names +genAlphaNum :: QC.Gen Char +genAlphaNum = QC.oneof [QC.chooseEnum ('a', 'z'), QC.chooseEnum ('A', 'Z'), QC.chooseEnum ('0', '9')] + +genUpperCamelCase :: Int -> QC.Gen Text +genUpperCamelCase len = do + h <- QC.chooseEnum ('A', 'Z') + t <- QC.vectorOf len genAlphaNum + return $ Text.pack $ h : t + +genModuleNamePart :: GenProto ModuleNamePart +genModuleNamePart = do + mnp <- lift . lift $ genUpperCamelCase 10 + return $ defMessage & name .~ mnp + +genModuleName :: GenProto ModuleName +genModuleName = do + ps <- chooseInt (1, 5) >>= vecOf genModuleNamePart + return $ defMessage & parts .~ ps + +genTyName :: GenProto TyName +genTyName = do + n <- lift . lift $ genUpperCamelCase 10 + return $ defMessage & name .~ n + +_genClassName :: GenProto ClassName +_genClassName = do + n <- lift . lift $ genUpperCamelCase 10 + return $ defMessage & name .~ n + +genConstrName :: GenProto ConstrName +genConstrName = do + n <- lift . lift $ genUpperCamelCase 10 + return $ defMessage & name .~ n + +genVarName :: GenProto VarName +genVarName = do + h <- lift . lift $ QC.chooseEnum ('a', 'z') + t <- lift . lift $ QC.vectorOf 4 (QC.chooseEnum ('a', 'z')) + return $ defMessage & name .~ Text.pack (h : t) + +genTyArg :: VarName -> GenProto TyArg +genTyArg vn = do + return $ + defMessage + & argName .~ vn + & argKind . kindRef .~ Kind'KIND_REF_TYPE -- TODO(bladyjoker): Gen arbitrary kinds. + +genSum :: [TyArg] -> GenProto Sum +genSum args = do + cns <- chooseInt (1, 10) >>= vecOf genConstrName + ctors <- for (List.nub cns) (genConstructor args) + return $ defMessage & constructors .~ ctors + +-- TODO(bladyjoker): Add TyRef, TyApp etc. +genTy :: [TyArg] -> GenProto Ty +genTy args = do + ar <- lift . lift $ QC.elements args + return $ defMessage & tyVar . varName .~ (ar ^. argName) + +genConstructor :: [TyArg] -> ConstrName -> GenProto Sum'Constructor +genConstructor args cn = do + tys <- chooseInt (1, 10) >>= vecOf (genTy args) + return $ + defMessage + & constrName .~ cn + & P.product . ntuple . fields .~ tys + +-- TODO(bladyjoker): Add Opaque. +genTyBody :: [TyArg] -> GenProto TyBody +genTyBody args = do + b <- genSum args + return $ defMessage & P.sum .~ b + +genTyAbs :: GenProto TyAbs +genTyAbs = do + vns <- chooseInt (1, 10) >>= vecOf genVarName + args <- for (List.nub vns) genTyArg + body <- genTyBody args + return $ + defMessage + & tyArgs .~ args + & tyBody .~ body + +genTyDef :: TyName -> GenProto TyDef +genTyDef tn = do + tyabs <- genTyAbs + return $ + defMessage + & tyName .~ tn + & tyAbs .~ tyabs + +genModule :: ModuleName -> GenProto Module +genModule mn = do + tns <- chooseInt (1, 100) >>= vecOf genTyName + tydefs <- for (List.nub tns) genTyDef + return $ + defMessage + & moduleName .~ mn + & typeDefs .~ tydefs + +genCompilerInput :: GenProto CompilerInput +genCompilerInput = do + mns <- chooseInt (1, 100) >>= vecOf genModuleName + ms <- for (List.nub mns) genModule + return $ defMessage & modules .~ ms From 0e2e1aa1b7dfa4faebb91d038dd5afa9d2c8ca74 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 17:22:35 +0100 Subject: [PATCH 12/20] Gen Proto tests rework --- .../app/LambdaBuffers/Compiler/Cli/Compile.hs | 17 +- .../lambda-buffers-compiler.cabal | 2 +- .../src/LambdaBuffers/Compiler/KindCheck.hs | 162 +++++++++--------- .../LambdaBuffers/Compiler/KindCheck/Kind.hs | 18 +- .../Compiler/ProtoCompat/FromProto.hs | 18 -- .../test/Test/KindCheck.hs | 2 +- .../test/Test/LambdaBuffers/Compiler.hs | 16 +- .../test/Test/LambdaBuffers/Compiler/Gen.hs | 71 ++++---- 8 files changed, 151 insertions(+), 155 deletions(-) diff --git a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs index 9ddca8c0..4db36e43 100644 --- a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs +++ b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs @@ -8,8 +8,7 @@ import Data.ProtoLens qualified as Pb import Data.ProtoLens.TextFormat qualified as PbText import Data.Text.Lazy qualified as Text import Data.Text.Lazy.IO qualified as Text -import LambdaBuffers.Compiler.KindCheck (check_) -import LambdaBuffers.Compiler.ProtoCompat (runFromProto, toProto) +import LambdaBuffers.Compiler (runCompiler) import Proto.Compiler (CompilerError, CompilerInput, CompilerOutput) import Proto.Compiler_Fields (compilerError, compilerResult) import System.FilePath.Lens (extension) @@ -28,17 +27,13 @@ makeLenses ''CompileOpts compile :: CompileOpts -> IO () compile opts = do compInp <- readCompilerInput (opts ^. input) - case runFromProto compInp of + case runCompiler compInp of Left compErr -> do - print @String "Encountered errors during CompilerInput proto parsing" + print @String "Encountered errors during Compilation" writeCompilerError (opts ^. output) compErr - Right compInp' -> do - print @String "Successfully parsed the CompilerInput proto" - case check_ compInp' of - Left kcCompErr -> do - print @String "Encountered errors during CompilerInput proto parsing" - writeCompilerError (opts ^. output) (toProto kcCompErr) - Right _ -> writeCompilerOutput (opts ^. output) (defMessage & compilerResult .~ defMessage) + Right compRes -> do + print @String "Compilation succeeded" + writeCompilerOutput (opts ^. output) (defMessage & compilerResult .~ compRes) return () readCompilerInput :: FilePath -> IO CompilerInput diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index 7c46932a..07b7c6f8 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -107,6 +107,7 @@ library , text >=1.2 exposed-modules: + LambdaBuffers.Compiler LambdaBuffers.Compiler.KindCheck LambdaBuffers.Compiler.KindCheck.Context LambdaBuffers.Compiler.KindCheck.Derivation @@ -155,7 +156,6 @@ test-suite tests , mtl >=2.2 , proto-lens >=0.7 , QuickCheck >=2.14 - , quickcheck-transformer , tasty >=1.4 , tasty-hunit >=0.10 , tasty-quickcheck >=0.10 diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 55dec00a..6944c5c0 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -35,17 +35,17 @@ import LambdaBuffers.Compiler.KindCheck.Inference ( infer, ) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I +import LambdaBuffers.Compiler.KindCheck.Kind (kind2ProtoKind) import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyEither, tyOpaque, tyProd, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef)) -import LambdaBuffers.Compiler.ProtoCompat (kind2ProtoKind) -import LambdaBuffers.Compiler.ProtoCompat.Types qualified as P -import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PT +import LambdaBuffers.Compiler.ProtoCompat () +import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC -------------------------------------------------------------------------------- -- Types -- | Kind Check failure types. -type CompilerErr = P.CompilerError +type CompilerErr = PC.CompilerError type Err = Error CompilerErr @@ -53,32 +53,32 @@ type ModName = [Text] -- | Main interface to the Kind Checker. data Check a where - KCheck :: P.CompilerInput -> Check Context + KCheck :: PC.CompilerInput -> Check Context makeEffect ''Check -- | Interactions that happen at the level of the Global Checker. data GlobalCheck a where - CreateContext :: P.CompilerInput -> GlobalCheck Context - ValidateModule :: Context -> P.Module -> GlobalCheck () + CreateContext :: PC.CompilerInput -> GlobalCheck Context + ValidateModule :: Context -> PC.Module -> GlobalCheck () makeEffect ''GlobalCheck -- | Interactions that happen at the level of the data ModuleCheck a where -- Module - KCTypeDefinition :: ModName -> Context -> P.TyDef -> ModuleCheck Kind - KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck () - KCClass :: Context -> P.ClassDef -> ModuleCheck () + KCTypeDefinition :: ModName -> Context -> PC.TyDef -> ModuleCheck Kind + KCClassInstance :: Context -> PC.InstanceClause -> ModuleCheck () + KCClass :: Context -> PC.ClassDef -> ModuleCheck () makeEffect ''ModuleCheck data KindCheck a where - KindFromTyDef :: ModName -> P.TyDef -> KindCheck Type - InferTypeKind :: ModName -> P.TyDef -> Context -> Type -> KindCheck Kind - CheckKindConsistency :: ModName -> P.TyDef -> Context -> Kind -> KindCheck Kind + KindFromTyDef :: ModName -> PC.TyDef -> KindCheck Type + InferTypeKind :: ModName -> PC.TyDef -> Context -> Type -> KindCheck Kind + CheckKindConsistency :: ModName -> PC.TyDef -> Context -> Kind -> KindCheck Kind -- FIXME(cstml): Add check for Context Consistency --- TyDefToTypes :: ModName -> P.TyDef -> KindCheck [Type] +-- TyDefToTypes :: ModName -> PC.TyDef -> KindCheck [Type] makeEffect ''KindCheck -------------------------------------------------------------------------------- @@ -90,11 +90,11 @@ runCheck = run . runError . runKindCheck . localStrategy . moduleStrategy . glob {- | Run the check - return the validated context or the failure. The main API function of the library. -} -check :: P.CompilerInput -> PT.CompilerOutput -check = fmap (const PT.CompilerResult) . runCheck . kCheck +check :: PC.CompilerInput -> PC.CompilerOutput +check = fmap (const PC.CompilerResult) . runCheck . kCheck -- | Run the check - drop the result if it succeeds - useful for testing. -check_ :: P.CompilerInput -> Either CompilerErr () +check_ :: PC.CompilerInput -> Either CompilerErr () check_ = void . runCheck . kCheck -------------------------------------------------------------------------------- @@ -115,7 +115,7 @@ globalStrategy = reinterpret $ \case moduleStrategy :: Transform GlobalCheck ModuleCheck moduleStrategy = reinterpret $ \case - CreateContext ci -> evalState (mempty @(M.Map Variable P.TyDef)) . resolveCreateContext $ ci + CreateContext ci -> evalState (mempty @(M.Map Variable PC.TyDef)) . resolveCreateContext $ ci ValidateModule cx md -> do traverse_ (kCTypeDefinition (module2ModuleName md) cx) (md ^. #typeDefs) traverse_ (kCClassInstance cx) (md ^. #instances) @@ -135,31 +135,31 @@ runKindCheck = interpret $ \case InferTypeKind _modName tyDef ctx ty -> either (handleErr tyDef) pure $ infer ctx ty CheckKindConsistency mname def ctx k -> runReader mname $ resolveKindConsistency def ctx k where - handleErr :: forall {b}. P.TyDef -> InferErr -> Eff effs b + handleErr :: forall {b}. PC.TyDef -> InferErr -> Eff effs b handleErr td = \case InferUnboundTermErr uA -> - throwError . P.CompKindCheckError $ P.UnboundTermError (tyDef2TyName td) (var2VarName uA) + throwError . PC.CompKindCheckError $ PC.UnboundTermError (tyDef2TyName td) (var2VarName uA) InferUnifyTermErr (I.Constraint (k1, k2)) -> - throwError . P.CompKindCheckError $ P.IncorrectApplicationError (tyDef2TyName td) (kind2ProtoKind k1) (kind2ProtoKind k2) + throwError . PC.CompKindCheckError $ PC.IncorrectApplicationError (tyDef2TyName td) (kind2ProtoKind k1) (kind2ProtoKind k2) InferRecursiveSubstitutionErr _ -> - throwError . P.CompKindCheckError $ P.RecursiveKindError $ tyDef2TyName td + throwError . PC.CompKindCheckError $ PC.RecursiveKindError $ tyDef2TyName td InferImpossibleErr t -> - throwError . P.InternalError $ t + throwError . PC.InternalError $ t var2VarName = \case - LocalRef n -> P.VarName n emptySourceInfo - ForeignRef m s -> P.VarName (intercalate "." m <> s) emptySourceInfo + LocalRef n -> PC.VarName n emptySourceInfo + ForeignRef m s -> PC.VarName (intercalate "." m <> s) emptySourceInfo - emptySourceInfo = P.SourceInfo mempty emptySourcePosition emptySourcePosition + emptySourceInfo = PC.SourceInfo mempty emptySourcePosition emptySourcePosition - emptySourcePosition = P.SourcePosition 0 0 + emptySourcePosition = PC.SourcePosition 0 0 -- Resolvers resolveKindConsistency :: forall effs. Members '[Reader ModName, Err] effs => - P.TyDef -> + PC.TyDef -> Context -> Kind -> Eff effs Kind @@ -170,15 +170,15 @@ resolveKindConsistency tydef _ctx inferredKind = do guard tyName k inferredKind pure inferredKind where - guard :: P.TyName -> Kind -> Kind -> Eff effs () + guard :: PC.TyName -> Kind -> Kind -> Eff effs () guard n i d | i == d = pure () | otherwise = - throwError . P.CompKindCheckError $ - P.InconsistentTypeError n (kind2ProtoKind i) (kind2ProtoKind d) + throwError . PC.CompKindCheckError $ + PC.InconsistentTypeError n (kind2ProtoKind i) (kind2ProtoKind d) -tyDef2TyName :: P.TyDef -> P.TyName -tyDef2TyName (P.TyDef n _ _) = n +tyDef2TyName :: PC.TyDef -> PC.TyName +tyDef2TyName (PC.TyDef n _ _) = n -------------------------------------------------------------------------------- -- Context Creation @@ -188,9 +188,9 @@ tyDef2TyName (P.TyDef n _ _) = n -} resolveCreateContext :: forall effs. - Member (State (M.Map Variable P.TyDef)) effs => + Member (State (M.Map Variable PC.TyDef)) effs => Member Err effs => - P.CompilerInput -> + PC.CompilerInput -> Eff effs Context resolveCreateContext ci = do ctxs <- traverse module2Context (toList $ ci ^. #modules) @@ -198,9 +198,9 @@ resolveCreateContext ci = do module2Context :: forall effs. - Member (State (M.Map Variable P.TyDef)) effs => + Member (State (M.Map Variable PC.TyDef)) effs => Member Err effs => - P.Module -> + PC.Module -> Eff effs Context module2Context m = do let typeDefinitions = toList $ m ^. #typeDefs @@ -211,11 +211,11 @@ module2Context m = do -- | Creates a Context entry from one type definition. tyDef2Context :: forall effs. - Member (Reader P.ModuleName) effs => - Member (State (M.Map Variable P.TyDef)) effs => + Member (Reader PC.ModuleName) effs => + Member (State (M.Map Variable PC.TyDef)) effs => Member Err effs => ModName -> - P.TyDef -> + PC.TyDef -> Eff effs Context tyDef2Context curModName tyDef = do r@(v, _) <- tyDef2NameAndKind curModName tyDef @@ -224,23 +224,23 @@ tyDef2Context curModName tyDef = do where -- Ads the name to our map - we can use its SourceLocation in the case of a -- double use. If it's already in our map - that means we've double declared it. - associateName :: Variable -> P.TyDef -> Eff effs () + associateName :: Variable -> PC.TyDef -> Eff effs () associateName v curTyDef = modify (M.insert v curTyDef) {- | Converts the Proto Module name to a local modname - dropping the information. -} -moduleName2ModName :: P.ModuleName -> ModName +moduleName2ModName :: PC.ModuleName -> ModName moduleName2ModName mName = (\p -> p ^. #name) <$> mName ^. #parts -tyDef2NameAndKind :: forall effs. ModName -> P.TyDef -> Eff effs (Variable, Kind) +tyDef2NameAndKind :: forall effs. ModName -> PC.TyDef -> Eff effs (Variable, Kind) tyDef2NameAndKind curModName tyDef = do -- all names are qualified let name = ForeignRef curModName (tyDef ^. #tyName . #name) let k = tyAbsLHS2Kind (tyDef ^. #tyAbs) pure (name, k) -tyAbsLHS2Kind :: P.TyAbs -> Kind +tyAbsLHS2Kind :: PC.TyAbs -> Kind tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Type . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs) foldWithArrow :: [Kind] -> Kind @@ -249,11 +249,11 @@ foldWithArrow = foldl (:->:) Type -- ================================================================================ -- To Kind Conversion functions -pKind2Type :: P.Kind -> Kind +pKind2Type :: PC.Kind -> Kind pKind2Type k = case k ^. #kind of - P.KindRef P.KType -> Type - P.KindArrow l r -> pKind2Type l :->: pKind2Type r + PC.KindRef PC.KType -> Type + PC.KindArrow l r -> pKind2Type l :->: pKind2Type r -- FIXME(cstml) what is an undefined type meant to mean? _ -> error "Fixme undefined type" @@ -263,19 +263,19 @@ pKind2Type k = tyDef2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.TyDef -> + PC.TyDef -> Eff eff Type tyDef2Type tyde = tyAbsLHS2Type (tyde ^. #tyAbs) <*> tyAbsRHS2Type (tyde ^. #tyAbs) tyAbsLHS2Type :: forall eff. - P.TyAbs -> + PC.TyAbs -> Eff eff (Type -> Type) tyAbsLHS2Type tyab = tyArgs2Type (toList $ tyab ^. #tyArgs) tyArgs2Type :: forall eff. - [P.TyArg] -> + [PC.TyArg] -> Eff eff (Type -> Type) tyArgs2Type = \case [] -> pure id @@ -283,59 +283,59 @@ tyArgs2Type = \case f <- tyArgs2Type xs pure $ \c -> Abs (tyArg2Var x) (f c) -tyArg2Var :: P.TyArg -> Variable +tyArg2Var :: PC.TyArg -> Variable tyArg2Var = LocalRef . view (#argName . #name) tyAbsRHS2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.TyAbs -> + PC.TyAbs -> Eff eff Type tyAbsRHS2Type tyab = tyBody2Type (tyab ^. #tyBody) tyBody2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.TyBody -> + PC.TyBody -> Eff eff Type tyBody2Type = \case - P.OpaqueI _ -> pure $ Var tyOpaque - P.SumI s -> sum2Type s + PC.OpaqueI _ -> pure $ Var tyOpaque + PC.SumI s -> sum2Type s sum2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Sum -> + PC.Sum -> Eff eff Type sum2Type su = foldWithSum <$> traverse constructor2Type (toList $ su ^. #constructors) constructor2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Constructor -> + PC.Constructor -> Eff eff Type constructor2Type co = product2Type (co ^. #product) product2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Product -> + PC.Product -> Eff eff Type product2Type = \case - P.RecordI r -> record2Type r - P.TupleI t -> tuple2Type t + PC.RecordI r -> record2Type r + PC.TupleI t -> tuple2Type t record2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Record -> + PC.Record -> Eff eff Type record2Type r = foldWithProduct <$> traverse field2Type (toList $ r ^. #fields) tuple2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Tuple -> + PC.Tuple -> Eff eff Type tuple2Type tu = do tup <- traverse ty2Type $ tu ^. #fields @@ -344,30 +344,30 @@ tuple2Type tu = do field2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Field -> + PC.Field -> Eff eff Type field2Type f = ty2Type (f ^. #fieldTy) ty2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.Ty -> + PC.Ty -> Eff eff Type ty2Type = \case - P.TyVarI tytv -> tyVar2Type tytv - P.TyAppI tyap -> tyApp2Type tyap - P.TyRefI tyre -> tyRef2Type tyre + PC.TyVarI tytv -> tyVar2Type tytv + PC.TyAppI tyap -> tyApp2Type tyap + PC.TyRefI tyre -> tyRef2Type tyre tyVar2Type :: forall eff. - P.TyVar -> + PC.TyVar -> Eff eff Type tyVar2Type tv = pure . Var . LocalRef $ (tv ^. #varName . #name) tyApp2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.TyApp -> + PC.TyApp -> Eff eff Type tyApp2Type ta = do fn <- ty2Type (ta ^. #tyFunc) @@ -377,16 +377,16 @@ tyApp2Type ta = do tyRef2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.TyRef -> + PC.TyRef -> Eff eff Type tyRef2Type = \case - P.LocalI lref -> localTyRef2Type lref - P.ForeignI fref -> foreignTyRef2Type fref + PC.LocalI lref -> localTyRef2Type lref + PC.ForeignI fref -> foreignTyRef2Type fref localTyRef2Type :: forall eff. Members '[Reader ModName, Err] eff => - P.LocalRef -> + PC.LocalRef -> Eff eff Type localTyRef2Type ltr = do moduleName <- ask @@ -394,7 +394,7 @@ localTyRef2Type ltr = do foreignTyRef2Type :: forall eff. - P.ForeignRef -> + PC.ForeignRef -> Eff eff Type foreignTyRef2Type ftr = do let moduleName = moduleName2ModName (ftr ^. #moduleName) @@ -407,7 +407,7 @@ foreignTyRef2Type ftr = do tyDef2Types :: forall eff. Members '[Reader ModName, Err] eff => - P.TyDef -> + PC.TyDef -> Eff eff [Type] tyDef2Types tyde = do f <- tyAbsLHS2Type (tyde ^. #tyAbs) -- abstraction @@ -417,23 +417,23 @@ tyDef2Types tyde = do tyAbsRHS2Types :: forall eff. Members '[Reader ModName, Err] eff => - P.TyAbs -> + PC.TyAbs -> Eff eff [Type] tyAbsRHS2Types tyab = tyBody2Types (tyab ^. #tyBody) tyBody2Types :: forall eff. Members '[Reader ModName, Err] eff => - P.TyBody -> + PC.TyBody -> Eff eff [Type] tyBody2Types = \case - P.OpaqueI _ -> pure [Var $ LocalRef "Opaque"] - P.SumI s -> sum2Types s + PC.OpaqueI _ -> pure [Var $ LocalRef "Opaque"] + PC.SumI s -> sum2Types s sum2Types :: forall eff. Members '[Reader ModName, Err] eff => - P.Sum -> + PC.Sum -> Eff eff [Type] sum2Types su = NonEmpty.toList <$> traverse constructor2Type (su ^. #constructors) -} @@ -449,5 +449,5 @@ foldWithProduct = foldl' (App . App (Var tyProd)) (Var tyUnit) foldWithSum :: [Type] -> Type foldWithSum = foldl' (App . App (Var tyEither)) (Var tyVoid) -module2ModuleName :: P.Module -> ModName +module2ModuleName :: PC.Module -> ModName module2ModuleName = moduleName2ModName . (^. #moduleName) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs index fb86df9d..e29482d7 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Kind.hs @@ -1,6 +1,7 @@ -module LambdaBuffers.Compiler.KindCheck.Kind (Kind (Type, (:->:), KVar)) where +module LambdaBuffers.Compiler.KindCheck.Kind (Kind (Type, (:->:), KVar), kind2ProtoKind, protoKind2Kind) where import LambdaBuffers.Compiler.KindCheck.Variable (Atom) +import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Prettyprinter (Pretty (pretty), parens, (<+>)) infixr 8 :->: @@ -17,3 +18,18 @@ instance Pretty Kind where ((x :->: y) :->: z) -> parens (pretty $ x :->: y) <+> "→" <+> pretty z x :->: y -> pretty x <+> "→" <+> pretty y KVar a -> pretty a + +-- | Convert from internal Kind to Proto Kind. +kind2ProtoKind :: Kind -> PC.Kind +kind2ProtoKind = \case + k1 :->: k2 -> PC.Kind $ PC.KindArrow (kind2ProtoKind k1) (kind2ProtoKind k2) + Type -> PC.Kind . PC.KindRef $ PC.KType + KVar _ -> PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen. + +-- | Convert from internal Kind to Proto Kind. +protoKind2Kind :: PC.Kind -> Kind +protoKind2Kind = \case + PC.Kind k -> case k of + PC.KindArrow k1 k2 -> protoKind2Kind k1 :->: protoKind2Kind k2 + PC.KindRef PC.KType -> Type + PC.KindRef PC.KUnspecified -> KVar "Unspecified" diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index a7938ef8..b347a360 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -1,6 +1,4 @@ module LambdaBuffers.Compiler.ProtoCompat.FromProto ( - protoKind2Kind, - kind2ProtoKind, runFromProto, toProto, ) where @@ -20,7 +18,6 @@ import Data.Set qualified as Set import Data.Text (Text) import Data.Text qualified as Text import GHC.Generics (Generic) -import LambdaBuffers.Compiler.KindCheck.Kind qualified as K import LambdaBuffers.Compiler.NamingCheck (checkClassName, checkConstrName, checkFieldName, checkModuleNamePart, checkTyName, checkVarName) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC import Proto.Compiler (NamingError) @@ -721,18 +718,3 @@ instance IsMessage P.CompilerOutput PC.CompilerOutput where toProto = \case Right res -> defMessage & P.compilerResult .~ toProto res Left err -> defMessage & P.compilerError .~ toProto err - --- | Convert from internal Kind to Proto Kind. -kind2ProtoKind :: K.Kind -> PC.Kind -kind2ProtoKind = \case - k1 K.:->: k2 -> PC.Kind $ PC.KindArrow (kind2ProtoKind k1) (kind2ProtoKind k2) - K.Type -> PC.Kind . PC.KindRef $ PC.KType - K.KVar _ -> PC.Kind . PC.KindRef $ PC.KUnspecified -- this shouldn't happen. - --- | Convert from internal Kind to Proto Kind. -protoKind2Kind :: PC.Kind -> K.Kind -protoKind2Kind = \case - PC.Kind k -> case k of - PC.KindArrow k1 k2 -> protoKind2Kind k1 K.:->: protoKind2Kind k2 - PC.KindRef PC.KType -> K.Type - PC.KindRef PC.KUnspecified -> K.KVar "Unspecified" diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index 7557bd12..6b310bac 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -22,7 +22,7 @@ import Test.QuickCheck ( (===), ) import Test.Tasty (TestTree, testGroup) -import Test.Tasty.HUnit (assertBool, assertEqual, testCase, (@?=)) +import Test.Tasty.HUnit (assertBool, testCase, (@?=)) import Test.Tasty.QuickCheck (testProperty) import Test.Utils.CompilerInput ( compilerInput'incoherent, diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs index d091c619..403c1209 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs @@ -1,6 +1,18 @@ module Test.LambdaBuffers.Compiler (test) where -import Test.Tasty (TestTree) +import Data.ProtoLens (Message (defMessage)) +import LambdaBuffers.Compiler (runCompiler) +import Test.LambdaBuffers.Compiler.Gen (genCompilerInput) +import Test.QuickCheck (forAll, (===)) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) test :: TestTree -test = undefined +test = + testGroup + "Compiler Proto API tests" + [ allCorrectCompInpCompile + ] + +allCorrectCompInpCompile :: TestTree +allCorrectCompInpCompile = testProperty "All correct CompilerInputs must compile" (forAll genCompilerInput (\compInp -> runCompiler compInp === Right defMessage)) diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs index de2ba463..3c086cda 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs @@ -1,8 +1,7 @@ module Test.LambdaBuffers.Compiler.Gen (genCompilerInput) where import Control.Lens ((&), (.~), (^.)) -import Control.Monad.Reader (MonadTrans (lift), ReaderT, replicateM) -import Control.Monad.State (StateT) +import Control.Monad.Reader (replicateM) import Data.List qualified as List import Data.ProtoLens (Message (defMessage)) import Data.Text (Text) @@ -13,17 +12,9 @@ import Proto.Compiler_Fields (argKind, argName, constrName, constructors, fields import Proto.Compiler_Fields qualified as P import Test.QuickCheck qualified as QC (Gen, chooseEnum, chooseInt, elements, oneof, vectorOf) -data GenProtoCtx -data GenProtoState - -type GenProto a = ReaderT GenProtoCtx (StateT GenProtoState QC.Gen) a - -vecOf :: forall {a}. GenProto a -> Int -> GenProto [a] +vecOf :: forall {a}. QC.Gen a -> Int -> QC.Gen [a] vecOf g n = replicateM n g -chooseInt :: (Int, Int) -> GenProto Int -chooseInt r = lift . lift $ QC.chooseInt r - -- | Names genAlphaNum :: QC.Gen Char genAlphaNum = QC.oneof [QC.chooseEnum ('a', 'z'), QC.chooseEnum ('A', 'Z'), QC.chooseEnum ('0', '9')] @@ -34,73 +25,73 @@ genUpperCamelCase len = do t <- QC.vectorOf len genAlphaNum return $ Text.pack $ h : t -genModuleNamePart :: GenProto ModuleNamePart +genModuleNamePart :: QC.Gen ModuleNamePart genModuleNamePart = do - mnp <- lift . lift $ genUpperCamelCase 10 + mnp <- genUpperCamelCase 10 return $ defMessage & name .~ mnp -genModuleName :: GenProto ModuleName +genModuleName :: QC.Gen ModuleName genModuleName = do - ps <- chooseInt (1, 5) >>= vecOf genModuleNamePart + ps <- QC.chooseInt (1, 5) >>= vecOf genModuleNamePart return $ defMessage & parts .~ ps -genTyName :: GenProto TyName +genTyName :: QC.Gen TyName genTyName = do - n <- lift . lift $ genUpperCamelCase 10 + n <- genUpperCamelCase 10 return $ defMessage & name .~ n -_genClassName :: GenProto ClassName +_genClassName :: QC.Gen ClassName _genClassName = do - n <- lift . lift $ genUpperCamelCase 10 + n <- genUpperCamelCase 10 return $ defMessage & name .~ n -genConstrName :: GenProto ConstrName +genConstrName :: QC.Gen ConstrName genConstrName = do - n <- lift . lift $ genUpperCamelCase 10 + n <- genUpperCamelCase 10 return $ defMessage & name .~ n -genVarName :: GenProto VarName +genVarName :: QC.Gen VarName genVarName = do - h <- lift . lift $ QC.chooseEnum ('a', 'z') - t <- lift . lift $ QC.vectorOf 4 (QC.chooseEnum ('a', 'z')) + h <- QC.chooseEnum ('a', 'z') + t <- QC.vectorOf 4 (QC.chooseEnum ('a', 'z')) return $ defMessage & name .~ Text.pack (h : t) -genTyArg :: VarName -> GenProto TyArg +genTyArg :: VarName -> QC.Gen TyArg genTyArg vn = do return $ defMessage & argName .~ vn - & argKind . kindRef .~ Kind'KIND_REF_TYPE -- TODO(bladyjoker): Gen arbitrary kinds. + & argKind . kindRef .~ Kind'KIND_REF_TYPE -- TODO(bladyjoker): QC.Gen arbitrary kinds. -genSum :: [TyArg] -> GenProto Sum +genSum :: [TyArg] -> QC.Gen Sum genSum args = do - cns <- chooseInt (1, 10) >>= vecOf genConstrName + cns <- QC.chooseInt (1, 2) >>= vecOf genConstrName ctors <- for (List.nub cns) (genConstructor args) return $ defMessage & constructors .~ ctors -- TODO(bladyjoker): Add TyRef, TyApp etc. -genTy :: [TyArg] -> GenProto Ty +genTy :: [TyArg] -> QC.Gen Ty genTy args = do - ar <- lift . lift $ QC.elements args + ar <- QC.elements args return $ defMessage & tyVar . varName .~ (ar ^. argName) -genConstructor :: [TyArg] -> ConstrName -> GenProto Sum'Constructor +genConstructor :: [TyArg] -> ConstrName -> QC.Gen Sum'Constructor genConstructor args cn = do - tys <- chooseInt (1, 10) >>= vecOf (genTy args) + tys <- QC.chooseInt (1, 2) >>= vecOf (genTy args) return $ defMessage & constrName .~ cn & P.product . ntuple . fields .~ tys -- TODO(bladyjoker): Add Opaque. -genTyBody :: [TyArg] -> GenProto TyBody +genTyBody :: [TyArg] -> QC.Gen TyBody genTyBody args = do b <- genSum args return $ defMessage & P.sum .~ b -genTyAbs :: GenProto TyAbs +genTyAbs :: QC.Gen TyAbs genTyAbs = do - vns <- chooseInt (1, 10) >>= vecOf genVarName + vns <- QC.chooseInt (1, 2) >>= vecOf genVarName args <- for (List.nub vns) genTyArg body <- genTyBody args return $ @@ -108,7 +99,7 @@ genTyAbs = do & tyArgs .~ args & tyBody .~ body -genTyDef :: TyName -> GenProto TyDef +genTyDef :: TyName -> QC.Gen TyDef genTyDef tn = do tyabs <- genTyAbs return $ @@ -116,17 +107,17 @@ genTyDef tn = do & tyName .~ tn & tyAbs .~ tyabs -genModule :: ModuleName -> GenProto Module +genModule :: ModuleName -> QC.Gen Module genModule mn = do - tns <- chooseInt (1, 100) >>= vecOf genTyName + tns <- QC.chooseInt (1, 2) >>= vecOf genTyName tydefs <- for (List.nub tns) genTyDef return $ defMessage & moduleName .~ mn & typeDefs .~ tydefs -genCompilerInput :: GenProto CompilerInput +genCompilerInput :: QC.Gen CompilerInput genCompilerInput = do - mns <- chooseInt (1, 100) >>= vecOf genModuleName + mns <- QC.chooseInt (1, 2) >>= vecOf genModuleName ms <- for (List.nub mns) genModule return $ defMessage & modules .~ ms From 21e9f8722eb825d8fc4afc925cdf1e05a357feeb Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 17:23:35 +0100 Subject: [PATCH 13/20] Forgot a file --- .../src/LambdaBuffers/Compiler.hs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs new file mode 100644 index 00000000..6d370d6b --- /dev/null +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs @@ -0,0 +1,16 @@ +module LambdaBuffers.Compiler (runCompiler) where + +import Data.ProtoLens (Message (defMessage)) +import LambdaBuffers.Compiler.KindCheck (check_) +import LambdaBuffers.Compiler.ProtoCompat.FromProto ( + runFromProto, + toProto, + ) +import Proto.Compiler (CompilerError, CompilerInput, CompilerResult) + +runCompiler :: CompilerInput -> Either CompilerError CompilerResult +runCompiler compInp = do + compInp' <- runFromProto compInp + case check_ compInp' of + Left err -> Left $ toProto err + Right _ -> Right defMessage From cc8f0d8f9031b398933ae295f8ad36d49cddb88c Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 17:27:08 +0100 Subject: [PATCH 14/20] Added warning about `stripSourceInfo` --- .../src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index b347a360..9272310c 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -88,6 +88,9 @@ parseAndIndex key = ) (mempty, mempty) +-- WARN(bladyjoker): This function is used to 'strip' the SourceInfo from types that end up as Map keys. +-- This can cause confusion and errors and we should rather parametrize types with `info` and +-- maintain `Map (TyName ()) (TyDef SourceInfo)` stripSourceInfo :: HasField "sourceInfo" s t a PC.SourceInfo => s -> t stripSourceInfo x = x & #sourceInfo .~ PC.defSourceInfo From d131862fb9d45c04e835632678f63948a7d6318e Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Tue, 14 Feb 2023 17:57:53 +0000 Subject: [PATCH 15/20] fix: foldr not foldl --- lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index ef4798dc..144abcf5 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -268,7 +268,7 @@ tyAbsLHS2Kind :: PC.TyAbs -> Kind tyAbsLHS2Kind tyAbs = foldWithArrow $ pKind2Kind . (\x -> x ^. #argKind) <$> toList (tyAbs ^. #tyArgs) foldWithArrow :: [Kind] -> Kind -foldWithArrow = foldl (:->:) Type +foldWithArrow = foldr (:->:) Type -- ================================================================================ -- To Kind Conversion functions From 4cc3480163b6a86dab232840dfa5e7ca5a3833dc Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 19:28:46 +0100 Subject: [PATCH 16/20] Proto documentation update --- .../Compiler/ProtoCompat/FromProto.hs | 4 +- .../test/Test/KindCheck.hs | 4 +- .../test/Test/TypeClassCheck.hs | 4 +- lambda-buffers-proto/compiler-proto.md | 330 +++++++++++------- lambda-buffers-proto/compiler.proto | 38 +- 5 files changed, 240 insertions(+), 140 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs index 9272310c..6c439818 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/FromProto.hs @@ -576,7 +576,7 @@ instance IsMessage P.Constraint PC.Constraint where fromProto c = do si <- fromProto $ c ^. P.sourceInfo cnm <- fromProto $ c ^. P.classRef - args <- traverse fromProto $ c ^. P.arguments + args <- traverse fromProto $ c ^. P.args arg <- case args of [] -> throwInternalError "Zero constraint arguments, but zero parameter type classes are not supported" [x] -> return x @@ -586,7 +586,7 @@ instance IsMessage P.Constraint PC.Constraint where toProto (PC.Constraint cnm arg si) = defMessage & P.classRef .~ toProto cnm - & P.arguments .~ pure (toProto arg) + & P.args .~ pure (toProto arg) & P.sourceInfo .~ toProto si {- diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index 6b310bac..404fec9a 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -76,8 +76,8 @@ kcTestOrdering = shuffledMods <- shuffle mods pure (_CompilerInput mods, _CompilerInput shuffledMods) -eitherFailOrPass :: forall {a} {c}. Either a c -> Either () () -eitherFailOrPass = bimap (const ()) (const ()) +_eitherFailOrPass :: forall {a} {c}. Either a c -> Either () () +_eitherFailOrPass = bimap (const ()) (const ()) -------------------------------------------------------------------------------- -- Fold tests diff --git a/lambda-buffers-compiler/test/Test/TypeClassCheck.hs b/lambda-buffers-compiler/test/Test/TypeClassCheck.hs index 547ae852..72daa44f 100644 --- a/lambda-buffers-compiler/test/Test/TypeClassCheck.hs +++ b/lambda-buffers-compiler/test/Test/TypeClassCheck.hs @@ -10,7 +10,7 @@ import LambdaBuffers.Compiler.ProtoCompat (runFromProto) import LambdaBuffers.Compiler.ProtoCompat.Types qualified as ProtoCompat import LambdaBuffers.Compiler.TypeClassCheck (detectSuperclassCycles') import Proto.Compiler (ClassDef, CompilerInput, Constraint, Kind, Kind'KindRef (Kind'KIND_REF_TYPE)) -import Proto.Compiler_Fields (argKind, argName, arguments, classArgs, classDefs, className, classRef, kindRef, localClassRef, moduleName, modules, name, parts, supers, tyVar, varName) +import Proto.Compiler_Fields (argKind, argName, args, classArgs, classDefs, className, classRef, kindRef, localClassRef, moduleName, modules, name, parts, supers, tyVar, varName) import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit (assertFailure, testCase, (@?=)) import Test.Utils.Constructors (_ModuleName) @@ -64,7 +64,7 @@ constraint :: Text -> Constraint constraint nm = defMessage & classRef . localClassRef . className . name .~ nm - & arguments .~ [defMessage & tyVar . varName . name .~ "a"] + & args .~ [defMessage & tyVar . varName . name .~ "a"] cycles :: CompilerInput cycles = diff --git a/lambda-buffers-proto/compiler-proto.md b/lambda-buffers-proto/compiler-proto.md index 5ab6541b..080ebaca 100644 --- a/lambda-buffers-proto/compiler-proto.md +++ b/lambda-buffers-proto/compiler-proto.md @@ -25,17 +25,22 @@ - [Module](#lambdabuffers-compiler-Module) - [ModuleName](#lambdabuffers-compiler-ModuleName) - [ModuleNamePart](#lambdabuffers-compiler-ModuleNamePart) - - [MultipleClassDefError](#lambdabuffers-compiler-MultipleClassDefError) - - [MultipleConstructorError](#lambdabuffers-compiler-MultipleConstructorError) - - [MultipleModuleError](#lambdabuffers-compiler-MultipleModuleError) - - [MultipleTyArgError](#lambdabuffers-compiler-MultipleTyArgError) - - [MultipleTyDefError](#lambdabuffers-compiler-MultipleTyDefError) - [NamingError](#lambdabuffers-compiler-NamingError) - [Opaque](#lambdabuffers-compiler-Opaque) - [Product](#lambdabuffers-compiler-Product) - [Product.NTuple](#lambdabuffers-compiler-Product-NTuple) - [Product.Record](#lambdabuffers-compiler-Product-Record) - [Product.Record.Field](#lambdabuffers-compiler-Product-Record-Field) + - [ProtoParseError](#lambdabuffers-compiler-ProtoParseError) + - [ProtoParseError.MultipleClassDefError](#lambdabuffers-compiler-ProtoParseError-MultipleClassDefError) + - [ProtoParseError.MultipleConstructorError](#lambdabuffers-compiler-ProtoParseError-MultipleConstructorError) + - [ProtoParseError.MultipleFieldError](#lambdabuffers-compiler-ProtoParseError-MultipleFieldError) + - [ProtoParseError.MultipleImportError](#lambdabuffers-compiler-ProtoParseError-MultipleImportError) + - [ProtoParseError.MultipleModuleError](#lambdabuffers-compiler-ProtoParseError-MultipleModuleError) + - [ProtoParseError.MultipleTyArgError](#lambdabuffers-compiler-ProtoParseError-MultipleTyArgError) + - [ProtoParseError.MultipleTyDefError](#lambdabuffers-compiler-ProtoParseError-MultipleTyDefError) + - [ProtoParseError.OneOfNotSetError](#lambdabuffers-compiler-ProtoParseError-OneOfNotSetError) + - [ProtoParseError.UnknownEnumError](#lambdabuffers-compiler-ProtoParseError-UnknownEnumError) - [SourceInfo](#lambdabuffers-compiler-SourceInfo) - [SourcePosition](#lambdabuffers-compiler-SourcePosition) - [Sum](#lambdabuffers-compiler-Sum) @@ -58,7 +63,6 @@ - [VarName](#lambdabuffers-compiler-VarName) - [Kind.KindRef](#lambdabuffers-compiler-Kind-KindRef) - - [NamingError.NameType](#lambdabuffers-compiler-NamingError-NameType) - [Scalar Value Types](#scalar-value-types) @@ -99,7 +103,7 @@ TODO(bladyjoker): Cleanup and reformulate with Sean. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | class_name | [ClassName](#lambdabuffers-compiler-ClassName) | | Type class name. | -| class_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | Type class arguments. Currently the Compiler only accepts single parameter type class declarations. | +| class_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | Type class arguments. Class with no arguments is a trivial class. Compiler MAY report an error. TODO(bladyjoker): MultipleClassArgError. | | supers | [Constraint](#lambdabuffers-compiler-Constraint) | repeated | Superclass constraints. | | documentation | [string](#string) | | Documentation elaborating on the type class. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -128,18 +132,15 @@ Type class name ### CompilerError -Compiler Error can be extended with other classes of errors. +Compiler Error | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| multiple_module_error | [MultipleModuleError](#lambdabuffers-compiler-MultipleModuleError) | | | -| multiple_tydef_error | [MultipleTyDefError](#lambdabuffers-compiler-MultipleTyDefError) | | | -| multiple_classdef_error | [MultipleClassDefError](#lambdabuffers-compiler-MultipleClassDefError) | | | -| multiple_tyarg_error | [MultipleTyArgError](#lambdabuffers-compiler-MultipleTyArgError) | | | -| multiple_constructor_error | [MultipleConstructorError](#lambdabuffers-compiler-MultipleConstructorError) | | | -| kind_check_error | [KindCheckError](#lambdabuffers-compiler-KindCheckError) | | | -| internal_error | [InternalError](#lambdabuffers-compiler-InternalError) | | | +| proto_parse_errors | [ProtoParseError](#lambdabuffers-compiler-ProtoParseError) | repeated | Errors occurred during proto parsing. | +| naming_errors | [NamingError](#lambdabuffers-compiler-NamingError) | repeated | Errors occurred during naming checking. | +| kind_check_errors | [KindCheckError](#lambdabuffers-compiler-KindCheckError) | repeated | Errors occurred during kind checking. | +| internal_errors | [InternalError](#lambdabuffers-compiler-InternalError) | repeated | Errors internal to the compiler implementation. | @@ -157,7 +158,7 @@ compilation closure needed by the Compiler to perform its task. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| modules | [Module](#lambdabuffers-compiler-Module) | repeated | Modules to compile. | +| modules | [Module](#lambdabuffers-compiler-Module) | repeated | Modules to compile. Duplicate modules MUST be reported with `ProtoParseError.MultipleModuleError`. | @@ -172,8 +173,8 @@ Output of the Compiler. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| compilation_error | [CompilerError](#lambdabuffers-compiler-CompilerError) | | | -| compilation_result | [CompilerResult](#lambdabuffers-compiler-CompilerResult) | | | +| compiler_error | [CompilerError](#lambdabuffers-compiler-CompilerError) | | | +| compiler_result | [CompilerResult](#lambdabuffers-compiler-CompilerResult) | | | @@ -185,8 +186,6 @@ Output of the Compiler. ### CompilerResult Compiler Result ~ a successful Compilation Output. -equivalent of unit. - @@ -217,7 +216,7 @@ Constraint expression | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | class_ref | [TyClassRef](#lambdabuffers-compiler-TyClassRef) | | Name of the type class. | -| arguments | [Ty](#lambdabuffers-compiler-Ty) | repeated | Constraint arguments. | +| args | [Ty](#lambdabuffers-compiler-Ty) | repeated | Constraint arguments. Constraint with no arguments is a trivial constraint. Compiler MAY report an error. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -244,7 +243,7 @@ Record type field name ### InstanceClause -Type class instances +Type class instances (rules) Instance clauses enable users to specify 'semantic' rules for their types. @@ -252,8 +251,8 @@ Instance clauses enable users to specify 'semantic' rules for their type | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | class_ref | [TyClassRef](#lambdabuffers-compiler-TyClassRef) | | Type class name. | -| heads | [Ty](#lambdabuffers-compiler-Ty) | repeated | Head of the instance clause. Currently, the Compiler only accepts single parameter type classes. | -| constraints | [Constraint](#lambdabuffers-compiler-Constraint) | repeated | Body of the rule, conjunction of constraints. | +| args | [Ty](#lambdabuffers-compiler-Ty) | repeated | Instance (rule) arguments. Instance clause with no arguments is a trivial instance clause. Compiler MAY report an error. | +| constraints | [Constraint](#lambdabuffers-compiler-Constraint) | repeated | Instance (rule) body, conjunction of constraints. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -269,7 +268,7 @@ Internal errors. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| internal_error | [string](#string) | | | +| msg | [string](#string) | | | @@ -375,7 +374,6 @@ The inferred type differs from the type as defined. ### KindCheckError.RecursiveKindError -Error reads: Inifinitely recursive term detected in definition ty_name. @@ -416,10 +414,10 @@ A module encapsulates type, class and instance definitions. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module name. | -| type_defs | [TyDef](#lambdabuffers-compiler-TyDef) | repeated | Type definitions. | -| class_defs | [ClassDef](#lambdabuffers-compiler-ClassDef) | repeated | Type class definitions. | +| type_defs | [TyDef](#lambdabuffers-compiler-TyDef) | repeated | Type definitions. Duplicate type definitions MUST be reported with `ProtoParseError.MultipleTyDefError`. | +| class_defs | [ClassDef](#lambdabuffers-compiler-ClassDef) | repeated | Type class definitions. Duplicate class definitions MUST be reported with `ProtoParseError.MultipleClassDefError`. | | instances | [InstanceClause](#lambdabuffers-compiler-InstanceClause) | repeated | Type class instance clauses. | -| imports | [ModuleName](#lambdabuffers-compiler-ModuleName) | repeated | Imported modules the Compiler consults when searching for instance clauses. | +| imports | [ModuleName](#lambdabuffers-compiler-ModuleName) | repeated | Imported modules the Compiler consults when searching for instance clauses. Duplicate imports MUST be reported with `ProtoParseError.MultipleImportError`. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -459,202 +457,301 @@ Module name part - + -### MultipleClassDefError -Multiple ClassDefs with the same ClassName were found in ModuleName. +### NamingError +Naming error message | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | -| class_defs | [ClassDef](#lambdabuffers-compiler-ClassDef) | repeated | Conflicting class definitions. | +| module_name_err | [ModuleNamePart](#lambdabuffers-compiler-ModuleNamePart) | | | +| ty_name_err | [TyName](#lambdabuffers-compiler-TyName) | | | +| var_name_err | [VarName](#lambdabuffers-compiler-VarName) | | | +| constr_name_err | [ConstrName](#lambdabuffers-compiler-ConstrName) | | | +| field_name_err | [FieldName](#lambdabuffers-compiler-FieldName) | | | +| class_name_err | [ClassName](#lambdabuffers-compiler-ClassName) | | | - + -### MultipleConstructorError -Multiple Sum Constructors with the same ConstrName were found in -ModuleName.TyDef. +### Opaque +Opaque type body + +A type that has an `Opaque` body represents a 'built-in' or a 'primitive' type +that's handled by the semantics 'under the hood'. It's called 'opaque' to denote +the fact that the Compiler has no knowledge of its structure, and relies that +the necessary knowledge is implemented elsewhere. The Codegen modules for any +target language have to be able to handle such types specifically and map to +existing value level representations and corresponding types. + +Codegen modules would have to implement support for such defined types, for +example: +- In Python `Set a` would map to `set()` from the standard library, +- In Haskell `Set a` would map to `containers`.Data.Set.Set type. + +Every `Opaque` type has to be considered deliberately for each language +environment targeted by Codegen modules. + +TODO(bladyjoker): Consider attaching explicit Kind terms to Opaques. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | -| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | -| constructors | [Sum.Constructor](#lambdabuffers-compiler-Sum-Constructor) | repeated | Conflicting constructors. | +| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | - + -### MultipleModuleError -Multiple Modules with the same ModuleName were found. +### Product +Product + +It's a built-in type term that exists enclosed within a [type abstraction](@ref +TyAbs) term which introduces [type variables](@ref TyVar) in the scope of the +expression. + +It exists in two flavors, either a Record or a NTuple. + +TODO(bladyjoker): Separate into Tuple and Record. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| modules | [Module](#lambdabuffers-compiler-Module) | repeated | Conflicting type definitions. | +| record | [Product.Record](#lambdabuffers-compiler-Product-Record) | | | +| ntuple | [Product.NTuple](#lambdabuffers-compiler-Product-NTuple) | | | - + -### MultipleTyArgError -Multiple TyArgs with the same ArgName were found in ModuleName.TyDef. +### Product.NTuple +A tuple type expression. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | -| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | -| ty_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | Conflicting type abstraction arguments. | +| fields | [Ty](#lambdabuffers-compiler-Ty) | repeated | Fields in a tuple are types. | +| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | - + + +### Product.Record +A record type expression. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| fields | [Product.Record.Field](#lambdabuffers-compiler-Product-Record-Field) | repeated | Record fields. | +| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | + + + + + + + + +### Product.Record.Field +Field in a record type. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| field_name | [FieldName](#lambdabuffers-compiler-FieldName) | | Record field name. | +| field_ty | [Ty](#lambdabuffers-compiler-Ty) | | Field type. | + + + + + + + + +### ProtoParseError +All errors that occur because of Google Protocol Buffer's inability to +enforce certain invariants. +Some of invariance: +- using Proto `map` restricts users to `string` keys which impacts + API documentation, which is why `repeated` fields are used throughout, +- using Proto 'oneof' means users have to check if such a field is + set or report an error otherwise. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| multiple_module_error | [ProtoParseError.MultipleModuleError](#lambdabuffers-compiler-ProtoParseError-MultipleModuleError) | | | +| multiple_tydef_error | [ProtoParseError.MultipleTyDefError](#lambdabuffers-compiler-ProtoParseError-MultipleTyDefError) | | | +| multiple_classdef_error | [ProtoParseError.MultipleClassDefError](#lambdabuffers-compiler-ProtoParseError-MultipleClassDefError) | | | +| multiple_tyarg_error | [ProtoParseError.MultipleTyArgError](#lambdabuffers-compiler-ProtoParseError-MultipleTyArgError) | | | +| multiple_constructor_error | [ProtoParseError.MultipleConstructorError](#lambdabuffers-compiler-ProtoParseError-MultipleConstructorError) | | | +| multiple_field_error | [ProtoParseError.MultipleFieldError](#lambdabuffers-compiler-ProtoParseError-MultipleFieldError) | | | +| multiple_import_error | [ProtoParseError.MultipleImportError](#lambdabuffers-compiler-ProtoParseError-MultipleImportError) | | | +| one_of_not_set_error | [ProtoParseError.OneOfNotSetError](#lambdabuffers-compiler-ProtoParseError-OneOfNotSetError) | | | +| unknown_enum_error | [ProtoParseError.UnknownEnumError](#lambdabuffers-compiler-ProtoParseError-UnknownEnumError) | | | + + -### MultipleTyDefError -Multiple TyDefs with the same TyName were found in ModuleName. + + + + + +### ProtoParseError.MultipleClassDefError +Multiple ClassDefs with the same ClassName were found in ModuleName. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | -| ty_defs | [TyDef](#lambdabuffers-compiler-TyDef) | repeated | Conflicting type definitions. | +| class_defs | [ClassDef](#lambdabuffers-compiler-ClassDef) | repeated | Conflicting class definitions. | - + -### NamingError -Naming error message +### ProtoParseError.MultipleConstructorError +Multiple Sum Constructors with the same ConstrName were found in +ModuleName.TyDef. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| name_type | [NamingError.NameType](#lambdabuffers-compiler-NamingError-NameType) | | Type of name. | -| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | +| constructors | [Sum.Constructor](#lambdabuffers-compiler-Sum-Constructor) | repeated | Conflicting constructors. | - + -### Opaque -Opaque type body +### ProtoParseError.MultipleFieldError +Multiple Record Fields with the same FieldName were found in +ModuleName.TyDef. -A type that has an `Opaque` body represents a 'built-in' or a 'primitive' type -that's handled by the semantics 'under the hood'. It's called 'opaque' to denote -the fact that the Compiler has no knowledge of its structure, and relies that -the necessary knowledge is implemented elsewhere. The Codegen modules for any -target language have to be able to handle such types specifically and map to -existing value level representations and corresponding types. -Codegen modules would have to implement support for such defined types, for -example: -- In Python `Set a` would map to `set()` from the standard library, -- In Haskell `Set a` would map to `containers`.Data.Set.Set type. +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | +| fields | [Product.Record.Field](#lambdabuffers-compiler-Product-Record-Field) | repeated | Conflicting record fields. | -Every `Opaque` type has to be considered deliberately for each language -environment targeted by Codegen modules. -TODO(bladyjoker): Consider attaching explicit Kind terms to Opaques. + + + + + + +### ProtoParseError.MultipleImportError + | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| imports | [ModuleName](#lambdabuffers-compiler-ModuleName) | repeated | Conflicting module imports. | - + + +### ProtoParseError.MultipleModuleError +Multiple Modules with the same ModuleName were found. + + +| Field | Type | Label | Description | +| ----- | ---- | ----- | ----------- | +| modules | [Module](#lambdabuffers-compiler-Module) | repeated | Conflicting type definitions. | + -### Product -Product -It's a built-in type term that exists enclosed within a [type abstraction](@ref -TyAbs) term which introduces [type variables](@ref TyVar) in the scope of the -expression. -It exists in two flavors, either a Record or a NTuple. -TODO(bladyjoker): Separate into Tuple and Record. + + + +### ProtoParseError.MultipleTyArgError +Multiple TyArgs with the same ArgName were found in ModuleName.TyDef. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| record | [Product.Record](#lambdabuffers-compiler-Product-Record) | | | -| ntuple | [Product.NTuple](#lambdabuffers-compiler-Product-NTuple) | | | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_def | [TyDef](#lambdabuffers-compiler-TyDef) | | Type definition in which the error was found. | +| ty_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | Conflicting type abstraction arguments. | - + -### Product.NTuple -A tuple type expression. +### ProtoParseError.MultipleTyDefError +Multiple TyDefs with the same TyName were found in ModuleName. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| fields | [Ty](#lambdabuffers-compiler-Ty) | repeated | Fields in a tuple are types. | -| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | +| module_name | [ModuleName](#lambdabuffers-compiler-ModuleName) | | Module in which the error was found. | +| ty_defs | [TyDef](#lambdabuffers-compiler-TyDef) | repeated | Conflicting type definitions. | - + -### Product.Record -A record type expression. +### ProtoParseError.OneOfNotSetError +Proto `oneof` field is not set. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| fields | [Product.Record.Field](#lambdabuffers-compiler-Product-Record-Field) | repeated | Record fields. | -| source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | +| message_name | [string](#string) | | Proto message name in which the `oneof` field is not set. | +| field_name | [string](#string) | | The `oneof` field that is not set. | - + -### Product.Record.Field -Field in a record type. +### ProtoParseError.UnknownEnumError +Proto `enum` field is unknown. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| field_name | [FieldName](#lambdabuffers-compiler-FieldName) | | Record field name. | -| field_ty | [Ty](#lambdabuffers-compiler-Ty) | | Field type. | +| enum_name | [string](#string) | | Proto `enum` name. | +| got_tag | [string](#string) | | The unknown tag for the `enum`. | @@ -728,12 +825,10 @@ type Foo_ a b = Either ) ``` -TODO(bladyjoker): Cleanup. - | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| constructors | [Sum.Constructor](#lambdabuffers-compiler-Sum-Constructor) | repeated | Sum type constructors. | +| constructors | [Sum.Constructor](#lambdabuffers-compiler-Sum-Constructor) | repeated | Sum type constructors. Empty `constructors` means `void` and means that the type can't be constructed. Compiler MAY report an error. Duplicate constructors MUST be reported with `ProtoParseError.MultipleConstructorError`. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -808,7 +903,7 @@ type term can only be introduced in the context of a | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | -| ty_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | List of type variables. | +| ty_args | [TyArg](#lambdabuffers-compiler-TyArg) | repeated | List of type variables. No type arguments means `delay` or `const ty_body`, meaning `TyAbs [] ty_body = ty_body`. Duplicate type arguments MUST be reported with `ProtoParseError.MultipleTyArgError`. | | ty_body | [TyBody](#lambdabuffers-compiler-TyBody) | | Type body. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -828,7 +923,7 @@ A type expression that applies a type abstraction to a list of arguments. | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | ty_func | [Ty](#lambdabuffers-compiler-Ty) | | Type function. TODO(bladyjoker): Rename to ty_abs? | -| ty_args | [Ty](#lambdabuffers-compiler-Ty) | repeated | Arguments to apply. | +| ty_args | [Ty](#lambdabuffers-compiler-Ty) | repeated | Arguments to apply. No arguments to apply means `force`, meaning `TyApp ty_func [] = ty_func`` | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -955,9 +1050,7 @@ Once introduced in the module scope, type definitions are referred to using | Field | Type | Label | Description | | ----- | ---- | ----- | ----------- | | ty_name | [TyName](#lambdabuffers-compiler-TyName) | | Type name. | -| ty_abs | [TyAbs](#lambdabuffers-compiler-TyAbs) | | Type term. - -TODO(bladyjoker): Turn into a oneOf TyAbs | Ty | +| ty_abs | [TyAbs](#lambdabuffers-compiler-TyAbs) | | Type term. | | source_info | [SourceInfo](#lambdabuffers-compiler-SourceInfo) | | Source information. | @@ -1093,23 +1186,6 @@ A built-in kind. | KIND_REF_TYPE | 1 | A `Type` kind (also know as `*` in Haskell) built-in. | - - - -### NamingError.NameType - - -| Name | Number | Description | -| ---- | ------ | ----------- | -| NAME_TYPE_UNSPECIFIED | 0 | | -| NAME_TYPE_MODULE | 1 | | -| NAME_TYPE_TYPE | 2 | | -| NAME_TYPE_VAR | 3 | | -| NAME_TYPE_CONSTR | 4 | | -| NAME_TYPE_FIELD | 5 | | -| NAME_TYPE_CLASS | 6 | | - - diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index 74f577a0..6427458d 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -77,6 +77,10 @@ type term can only be introduced in the context of a */ message TyAbs { // List of type variables. + // No type arguments means `delay` or `const ty_body`, + // meaning `TyAbs [] ty_body = ty_body`. + // Duplicate type arguments MUST be reported with + // `ProtoParseError.MultipleTyArgError`. repeated TyArg ty_args = 1; // Type body. TyBody ty_body = 2; @@ -92,6 +96,7 @@ message TyApp { // Type function. TODO(bladyjoker): Rename to ty_abs? Ty ty_func = 1; // Arguments to apply. + // No arguments to apply means `force`, meaning `TyApp ty_func [] = ty_func`` repeated Ty ty_args = 2; // Source information. SourceInfo source_info = 3; @@ -206,7 +211,7 @@ message TyDef { // Type name. TyName ty_name = 1; // Type term. - TyAbs ty_abs = 2; // TODO(bladyjoker): Turn into a oneOf TyAbs | Ty + TyAbs ty_abs = 2; // Source information. SourceInfo source_info = 3; } @@ -327,8 +332,6 @@ type Foo_ a b = Either (b, ConstrName) ) ``` - -TODO(bladyjoker): Cleanup. */ message Sum { // Constructor of a Sum type is a Product type term. @@ -341,6 +344,10 @@ message Sum { Product product = 2; }; // Sum type constructors. + // Empty `constructors` means `void` and means that the type can't be + // constructed. Compiler MAY report an error. + // Duplicate constructors MUST be reported with + // `ProtoParseError.MultipleConstructorError`. repeated Constructor constructors = 1; // Source information. SourceInfo source_info = 2; @@ -379,6 +386,9 @@ message Product { SourceInfo source_info = 2; } // A product is a record or a tuple. + // A record or a tuple with no fields means `unit`. + // Duplicate fields in a record MUST be reported with + // `ProtoParseError.MultipleFieldError`. oneof product { Record record = 1; NTuple ntuple = 2; @@ -409,8 +419,9 @@ TODO(bladyjoker): Cleanup and reformulate with Sean. message ClassDef { // Type class name. ClassName class_name = 1; - // Type class arguments. Currently the Compiler only accepts single parameter - // type class declarations. + // Type class arguments. + // Class with no arguments is a trivial class. Compiler MAY report an error. + // TODO(bladyjoker): MultipleClassArgError. repeated TyArg class_args = 2; // Superclass constraints. repeated Constraint supers = 3; @@ -460,6 +471,8 @@ message InstanceClause { // Type class name. TyClassRef class_ref = 1; // Instance (rule) arguments. + // Instance clause with no arguments is a trivial instance clause. + // Compiler MAY report an error. repeated Ty args = 2; // Instance (rule) body, conjunction of constraints. repeated Constraint constraints = 3; @@ -472,7 +485,9 @@ message Constraint { // Name of the type class. TyClassRef class_ref = 1; // Constraint arguments. - repeated Ty arguments = 2; + // Constraint with no arguments is a trivial constraint. + // Compiler MAY report an error. + repeated Ty args = 2; // Source information. SourceInfo source_info = 3; } @@ -485,12 +500,19 @@ message Module { // Module name. ModuleName module_name = 1; // Type definitions. + // Duplicate type definitions MUST be reported with + // `ProtoParseError.MultipleTyDefError`. repeated TyDef type_defs = 2; // Type class definitions. + // Duplicate class definitions MUST be reported with + // `ProtoParseError.MultipleClassDefError`. repeated ClassDef class_defs = 3; // Type class instance clauses. repeated InstanceClause instances = 4; - // Imported modules the Compiler consults when searching for instance clauses. + // Imported modules the Compiler consults when searching for + // instance clauses. + // Duplicate imports MUST be reported with + // `ProtoParseError.MultipleImportError`. repeated ModuleName imports = 5; // Source information. SourceInfo source_info = 6; @@ -503,6 +525,8 @@ compilation closure needed by the Compiler to perform its task. */ message CompilerInput { // Modules to compile. + // Duplicate modules MUST be reported with + // `ProtoParseError.MultipleModuleError`. repeated Module modules = 1; } From 409ef18c415175512dead3608a5ba951d2922205 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 19:37:38 +0100 Subject: [PATCH 17/20] Remove a failing test and added TODOs, cleaned up after merge --- .../test/Test/KindCheck.hs | 26 +------------------ .../test/Test/LambdaBuffers/Compiler.hs | 3 +++ .../test/Test/LambdaBuffers/Compiler/Gen.hs | 15 ++++++----- 3 files changed, 13 insertions(+), 31 deletions(-) diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index 404fec9a..e289a3f8 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -1,6 +1,5 @@ module Test.KindCheck (test) where -import Data.Bifunctor (Bifunctor (bimap)) import Data.Text (Text) import LambdaBuffers.Compiler.KindCheck ( check_, @@ -17,8 +16,6 @@ import Test.QuickCheck ( Property, forAll, forAllShrink, - resize, - shuffle, (===), ) import Test.Tasty (TestTree, testGroup) @@ -40,7 +37,7 @@ test = testGroup "Compiler tests" [testCheck, testFolds, testRefl] -- Module tests testCheck :: TestTree -testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe, kcTestFailing, kcTestOrdering] +testCheck = testGroup "KindChecker Tests" [trivialKCTest, kcTestMaybe, kcTestFailing] trivialKCTest :: TestTree trivialKCTest = @@ -58,27 +55,6 @@ kcTestFailing = assertBool "Test should have failed" $ check_ compilerInput'incoherent /= Right () -{- | TyDef order does not matter when kind checking. - - We're not interested in the failure error as there might be more than two - errors in a module - and it is non-determistic which one is first. But it is - deterministic if the property holds for the whole CompilerInput. Therefore we - only track if given the input - the fails or succeeds. --} -kcTestOrdering :: TestTree -kcTestOrdering = - testProperty "Module order inside the CompilerInput does not matter" $ - forAllShrink (resize 2 genModuleIn2Layouts) shrink $ - \(l, r) -> check_ l === check_ r - where - genModuleIn2Layouts = do - mods <- arbitrary - shuffledMods <- shuffle mods - pure (_CompilerInput mods, _CompilerInput shuffledMods) - -_eitherFailOrPass :: forall {a} {c}. Either a c -> Either () () -_eitherFailOrPass = bimap (const ()) (const ()) - -------------------------------------------------------------------------------- -- Fold tests diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs index 403c1209..74932563 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs @@ -16,3 +16,6 @@ test = allCorrectCompInpCompile :: TestTree allCorrectCompInpCompile = testProperty "All correct CompilerInputs must compile" (forAll genCompilerInput (\compInp -> runCompiler compInp === Right defMessage)) + +-- TODO(bladyjoker): Add error producing mutations. +-- TODO(bladyjoker): Add bening mutations (module, tydef, classdef shuffle). diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs index 3c086cda..a19cef37 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/Gen.hs @@ -15,6 +15,9 @@ import Test.QuickCheck qualified as QC (Gen, chooseEnum, chooseInt, elements, on vecOf :: forall {a}. QC.Gen a -> Int -> QC.Gen [a] vecOf g n = replicateM n g +limit :: Int +limit = 10 + -- | Names genAlphaNum :: QC.Gen Char genAlphaNum = QC.oneof [QC.chooseEnum ('a', 'z'), QC.chooseEnum ('A', 'Z'), QC.chooseEnum ('0', '9')] @@ -32,7 +35,7 @@ genModuleNamePart = do genModuleName :: QC.Gen ModuleName genModuleName = do - ps <- QC.chooseInt (1, 5) >>= vecOf genModuleNamePart + ps <- QC.chooseInt (1, limit) >>= vecOf genModuleNamePart return $ defMessage & parts .~ ps genTyName :: QC.Gen TyName @@ -65,7 +68,7 @@ genTyArg vn = do genSum :: [TyArg] -> QC.Gen Sum genSum args = do - cns <- QC.chooseInt (1, 2) >>= vecOf genConstrName + cns <- QC.chooseInt (1, limit) >>= vecOf genConstrName ctors <- for (List.nub cns) (genConstructor args) return $ defMessage & constructors .~ ctors @@ -77,7 +80,7 @@ genTy args = do genConstructor :: [TyArg] -> ConstrName -> QC.Gen Sum'Constructor genConstructor args cn = do - tys <- QC.chooseInt (1, 2) >>= vecOf (genTy args) + tys <- QC.chooseInt (1, limit) >>= vecOf (genTy args) return $ defMessage & constrName .~ cn @@ -91,7 +94,7 @@ genTyBody args = do genTyAbs :: QC.Gen TyAbs genTyAbs = do - vns <- QC.chooseInt (1, 2) >>= vecOf genVarName + vns <- QC.chooseInt (1, limit) >>= vecOf genVarName args <- for (List.nub vns) genTyArg body <- genTyBody args return $ @@ -109,7 +112,7 @@ genTyDef tn = do genModule :: ModuleName -> QC.Gen Module genModule mn = do - tns <- QC.chooseInt (1, 2) >>= vecOf genTyName + tns <- QC.chooseInt (1, limit) >>= vecOf genTyName tydefs <- for (List.nub tns) genTyDef return $ defMessage @@ -118,6 +121,6 @@ genModule mn = do genCompilerInput :: QC.Gen CompilerInput genCompilerInput = do - mns <- QC.chooseInt (1, 2) >>= vecOf genModuleName + mns <- QC.chooseInt (1, limit) >>= vecOf genModuleName ms <- for (List.nub mns) genModule return $ defMessage & modules .~ ms From 39e0700c8a280e929e715f87e7a309f69f545c70 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 14 Feb 2023 19:50:33 +0100 Subject: [PATCH 18/20] Applied review suggestions --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 4 ++-- .../Compiler/KindCheck/Inference.hs | 4 ++-- .../src/LambdaBuffers/Compiler/KindCheck/Type.hs | 6 +++--- .../LambdaBuffers/Compiler/ProtoCompat/Types.hs | 7 +++++++ lambda-buffers-compiler/test/Test/KindCheck.hs | 16 ++++++++-------- 5 files changed, 22 insertions(+), 15 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 144abcf5..38e90c16 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -36,7 +36,7 @@ import LambdaBuffers.Compiler.KindCheck.Inference ( ) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I import LambdaBuffers.Compiler.KindCheck.Kind (kind2ProtoKind) -import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyEither, tyProd, tyUnit, tyVoid) +import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyProd, tySum, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef)) import LambdaBuffers.Compiler.ProtoCompat () import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC @@ -479,7 +479,7 @@ foldWithProduct :: [Type] -> Type foldWithProduct = foldl' (App . App (Var tyProd)) (Var tyUnit) foldWithSum :: [Type] -> Type -foldWithSum = foldl' (App . App (Var tyEither)) (Var tyVoid) +foldWithSum = foldl' (App . App (Var tySum)) (Var tyVoid) module2ModuleName :: PC.Module -> ModName module2ModuleName = moduleName2ModName . (^. #moduleName) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index 47225610..c97938b9 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -21,7 +21,7 @@ import LambdaBuffers.Compiler.KindCheck.Context (Context (Context), addContext, import LambdaBuffers.Compiler.KindCheck.Derivation (Derivation (Abstraction, Application, Axiom)) import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement (Judgement)) import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KVar, Type, (:->:))) -import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyEither, tyProd, tyUnit, tyVoid) +import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyProd, tySum, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable) import Control.Monad.Freer (Eff, Member, Members, run) @@ -96,7 +96,7 @@ infer ctx t = do mempty & context .~ M.fromList - [ (tyEither, Type :->: Type :->: Type) + [ (tySum, Type :->: Type :->: Type) , (tyProd, Type :->: Type :->: Type) , (tyUnit, Type) , (tyVoid, Type) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs index 3a84731d..aa333b0e 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Type.hs @@ -7,7 +7,7 @@ module LambdaBuffers.Compiler.KindCheck.Type ( tyOpaque, tyUnit, tyVoid, - tyEither, + tySum, tyProd, ) where @@ -30,8 +30,8 @@ tyUnit = LocalRef "𝟙" tyVoid :: Variable tyVoid = LocalRef "𝟘" -tyEither :: Variable -tyEither = LocalRef "Σ" +tySum :: Variable +tySum = LocalRef "Σ" tyProd :: Variable tyProd = LocalRef "Π" diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs index 617ae009..e3334098 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/ProtoCompat/Types.hs @@ -69,6 +69,13 @@ data SourcePosition = SourcePosition {column :: Int, row :: Int} deriving stock (Show, Eq, Ord, Generic) deriving (Arbitrary) via GenericArbitrary SourcePosition +-- TODO(bladyjoker): Make this proper by parametrized SourceInfo as `info`. For +-- example, `TyName` becomes `TyName info` and when working with `TyName +-- SourceInfo` a 'stripped' version can be obtained by simply `void tyName :: +-- TyName ()`. +-- In situations like testing or indexing when we want to ignore the SourceInfo, +-- this seems like the proper way of doing it. Then we wouldn't need +-- `defSourceInfo`. defSourceInfo :: SourceInfo defSourceInfo = SourceInfo "" (SourcePosition 0 0) (SourcePosition 0 0) diff --git a/lambda-buffers-compiler/test/Test/KindCheck.hs b/lambda-buffers-compiler/test/Test/KindCheck.hs index e289a3f8..f91287b5 100644 --- a/lambda-buffers-compiler/test/Test/KindCheck.hs +++ b/lambda-buffers-compiler/test/Test/KindCheck.hs @@ -6,7 +6,7 @@ import LambdaBuffers.Compiler.KindCheck ( foldWithProduct, foldWithSum, ) -import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var), tyEither, tyProd, tyUnit, tyVoid) +import LambdaBuffers.Compiler.KindCheck.Type (Type (App, Var), tyProd, tySum, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable ( Variable (LocalRef), ) @@ -104,8 +104,8 @@ testPProdFoldTotal = forAll arbitrary $ \ts -> foldWithProduct ts === foldWithProduct ts -either' :: Type -> Type -> Type -either' = App . App (Var tyEither) +sum' :: Type -> Type -> Type +sum' = App . App (Var tySum) void' :: Type void' = Var tyVoid @@ -116,25 +116,25 @@ testSumFold0 = testCase "Fold 0 type" $ foldWithSum [] @?= void' --- | [ a ] -> either void a +-- | [ a ] -> sum void a testSumFold1 :: TestTree testSumFold1 = testCase "Fold 1 type" $ - foldWithSum [lVar "a"] @?= either' void' (lVar "a") + foldWithSum [lVar "a"] @?= sum' void' (lVar "a") --- | [ a , b ] -> either (either void a) b +-- | [ a , b ] -> sum (sum void a) b testSumFold2 :: TestTree testSumFold2 = testCase "Fold 2 type" $ foldWithSum [lVar "b", lVar "a"] - @?= either' (either' void' (lVar "b")) (lVar "a") + @?= sum' (sum' void' (lVar "b")) (lVar "a") -- | [ a , b , c ] -> a | ( b | c ) testSumFold3 :: TestTree testSumFold3 = testCase "Fold 3 types" $ foldWithSum [lVar "c", lVar "b", lVar "a"] - @?= either' (either' (either' void' (lVar "c")) (lVar "b")) (lVar "a") + @?= sum' (sum' (sum' void' (lVar "c")) (lVar "b")) (lVar "a") -- | TyDef to Kind Canonical representation - sums not folded - therefore we get constructor granularity. Might use in a different implementation for more granular errors. lVar :: Text -> Type From d243b4f5630cbb40d46398336e980ab716faae42 Mon Sep 17 00:00:00 2001 From: "Vlad P. Luchian" Date: Wed, 15 Feb 2023 11:56:28 +0000 Subject: [PATCH 19/20] fix: add opaque to context --- .../src/LambdaBuffers/Compiler/KindCheck.hs | 4 +-- .../Compiler/KindCheck/Inference.hs | 27 ++++++++++--------- 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index 38e90c16..d07ee7ca 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -36,7 +36,7 @@ import LambdaBuffers.Compiler.KindCheck.Inference ( ) import LambdaBuffers.Compiler.KindCheck.Inference qualified as I import LambdaBuffers.Compiler.KindCheck.Kind (kind2ProtoKind) -import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyProd, tySum, tyUnit, tyVoid) +import LambdaBuffers.Compiler.KindCheck.Type (Type (App), tyOpaque, tyProd, tySum, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable (Variable (ForeignRef, LocalRef)) import LambdaBuffers.Compiler.ProtoCompat () import LambdaBuffers.Compiler.ProtoCompat.Types qualified as PC @@ -459,7 +459,7 @@ tyBody2Types :: PC.TyBody -> Eff eff [Type] tyBody2Types = \case - PC.OpaqueI _ -> pure [Var $ LocalRef "Opaque"] + PC.OpaqueI _ -> pure [Var tyOpaque] PC.SumI s -> sum2Types s sum2Types :: diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs index c97938b9..ca1b8114 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck/Inference.hs @@ -21,7 +21,7 @@ import LambdaBuffers.Compiler.KindCheck.Context (Context (Context), addContext, import LambdaBuffers.Compiler.KindCheck.Derivation (Derivation (Abstraction, Application, Axiom)) import LambdaBuffers.Compiler.KindCheck.Judgement (Judgement (Judgement)) import LambdaBuffers.Compiler.KindCheck.Kind (Kind (KVar, Type, (:->:))) -import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyProd, tySum, tyUnit, tyVoid) +import LambdaBuffers.Compiler.KindCheck.Type (Type (Abs, App, Var), tyOpaque, tyProd, tySum, tyUnit, tyVoid) import LambdaBuffers.Compiler.KindCheck.Variable (Atom, Variable) import Control.Monad.Freer (Eff, Member, Members, run) @@ -87,20 +87,23 @@ runDerive ctx t = run $ runError $ runWriter $ evalState (DC atoms) $ runReader infer :: Context -> Type -> Either InferErr Kind infer ctx t = do - (d, c) <- runDerive (defTerms <> ctx) t + (d, c) <- runDerive (defContext <> ctx) t s <- runUnify' c let res = foldl (flip substitute) d s pure $ res ^. topKind - where - defTerms = - mempty - & context - .~ M.fromList - [ (tySum, Type :->: Type :->: Type) - , (tyProd, Type :->: Type :->: Type) - , (tyUnit, Type) - , (tyVoid, Type) - ] + +-- | Default KC Context. +defContext :: Context +defContext = + mempty + & context + .~ M.fromList + [ (tySum, Type :->: Type :->: Type) + , (tyProd, Type :->: Type :->: Type) + , (tyUnit, Type) + , (tyVoid, Type) + , (tyOpaque, Type) + ] -------------------------------------------------------------------------------- -- Implementation From 54100bdd09577313cb1454aa41a205e1cdadc544 Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Wed, 15 Feb 2023 13:26:57 +0100 Subject: [PATCH 20/20] Applied suggestions --- .../app/LambdaBuffers/Compiler/Cli/Compile.hs | 4 ++-- .../src/LambdaBuffers/Compiler/KindCheck.hs | 7 ++----- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs index 4db36e43..83741570 100644 --- a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs +++ b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs @@ -29,10 +29,10 @@ compile opts = do compInp <- readCompilerInput (opts ^. input) case runCompiler compInp of Left compErr -> do - print @String "Encountered errors during Compilation" + putStrLn "Encountered errors during Compilation" writeCompilerError (opts ^. output) compErr Right compRes -> do - print @String "Compilation succeeded" + putStrLn "Compilation succeeded" writeCompilerOutput (opts ^. output) (defMessage & compilerResult .~ compRes) return () diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs index d07ee7ca..1d33aa96 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/KindCheck.hs @@ -68,7 +68,7 @@ makeEffect ''GlobalCheck data ModuleCheck a where -- Module KCTypeDefinition :: ModName -> Context -> PC.TyDef -> ModuleCheck Kind --- fixme(cstml & gnumonik): lets reach consensus on these - Note(1). +-- NOTE(cstml & gnumonik): Lets reach consensus on these - Note(1). -- KCClassInstance :: Context -> P.InstanceClause -> ModuleCheck () -- KCClass :: Context -> P.ClassDef -> ModuleCheck () @@ -79,8 +79,6 @@ data KindCheck a where InferTypeKind :: ModName -> PC.TyDef -> Context -> Type -> KindCheck Kind CheckKindConsistency :: ModName -> PC.TyDef -> Context -> Kind -> KindCheck Kind --- TypeFromTyDef :: ModName -> P.TyDef -> KindCheck Type -- replaced with constructor by constructor check - makeEffect ''KindCheck -------------------------------------------------------------------------------- @@ -139,7 +137,6 @@ localStrategy = reinterpret $ \case runKindCheck :: forall effs {a}. Member Err effs => Eff (KindCheck ': effs) a -> Eff effs a runKindCheck = interpret $ \case - -- TypeFromTyDef moduleName tydef -> runReader moduleName (tyDef2Type tydef) TypesFromTyDef moduleName tydef -> runReader moduleName (tyDef2Types tydef) InferTypeKind _modName tyDef ctx ty -> either (handleErr tyDef) pure $ infer ctx ty CheckKindConsistency mname def ctx k -> runReader mname $ resolveKindConsistency def ctx k @@ -278,7 +275,7 @@ pKind2Kind k = case k ^. #kind of PC.KindRef PC.KType -> Type PC.KindArrow l r -> pKind2Kind l :->: pKind2Kind r - -- FIXME(cstml) what is an undefined type meant to mean? + -- NOTE(cstml): What is an Kind type meant to mean? _ -> error "Fixme undefined type" -- =============================================================================