Skip to content
This repository was archived by the owner on Jan 12, 2024. It is now read-only.

Use HM inference in expression and statement verification #940

Merged
merged 17 commits into from
Apr 8, 2021
Merged

Use HM inference in expression and statement verification #940

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
4e3b7fe
Use HM inference in expression and statement verification
Mar 31, 2021
cc68e30
Update comments
Mar 31, 2021
0f64224
Deprecate diagnostics
Mar 31, 2021
469307f
Merge branch 'feature/qep2' into samarsha/hm-inference
bamarsha Mar 31, 2021
c9cfd3b
Update doc comments in ExpressionVerification.fs
Mar 31, 2021
b2bdd30
Update LocalVerification.qs
Apr 1, 2021
f29a177
Use OperationCallOutsideOfOperation diagnostic
Apr 1, 2021
dd807b6
Deprecate MissingExprInArray diagnostic
Apr 6, 2021
2cffa7a
Remove replaceTypeParams
Apr 6, 2021
622e680
Remove VerifyNumberedItemAccess
Apr 6, 2021
5ca9c9a
Rename VerifyArrayItem
Apr 6, 2021
5202271
Add doc comment to partialArgType
Apr 6, 2021
dbeca8b
Update naming convention
Apr 6, 2021
12b7405
Nicer exprWithoutTypeArgs
Apr 6, 2021
83002e6
Clean up exprWithoutTypeArgs again
Apr 7, 2021
605df35
Rename verifyConcatenation
Apr 7, 2021
fb25d58
Update verifyUdtWith documentation
Apr 7, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 20 additions & 8 deletions src/QsCompiler/CompilationManager/TypeChecking.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,17 +7,20 @@
using System.Diagnostics.CodeAnalysis;
using System.Linq;
using System.Threading;

using Microsoft.Quantum.QsCompiler.CompilationBuilder.DataStructures;
using Microsoft.Quantum.QsCompiler.DataTypes;
using Microsoft.Quantum.QsCompiler.DependencyAnalysis;
using Microsoft.Quantum.QsCompiler.Diagnostics;
using Microsoft.Quantum.QsCompiler.SymbolManagement;
using Microsoft.Quantum.QsCompiler.SyntaxProcessing;
using Microsoft.Quantum.QsCompiler.SyntaxProcessing.TypeInference;
using Microsoft.Quantum.QsCompiler.SyntaxTokens;
using Microsoft.Quantum.QsCompiler.SyntaxTree;
using Microsoft.Quantum.QsCompiler.TextProcessing;
using Microsoft.Quantum.QsCompiler.Transformations;
using Microsoft.VisualStudio.LanguageServer.Protocol;

using Position = Microsoft.Quantum.QsCompiler.DataTypes.Position;
using Range = Microsoft.Quantum.QsCompiler.DataTypes.Range;

Expand Down Expand Up @@ -591,10 +594,14 @@ private static T BuildStatement<T>(
ScopeContext context,
List<Diagnostic> diagnostics)
{
var statementPos = node.Fragment.Range.Start;
var statementPosition = node.Fragment.Range.Start;
context.Inference.UseStatementPosition(statementPosition);

var location = new QsLocation(node.RelativePosition, node.Fragment.HeaderRange);
var (statement, messages) = build(location, context);
diagnostics.AddRange(messages.Select(msg => Diagnostics.Generate(context.Symbols.SourceFile, msg, statementPos)));
var (statement, buildDiagnostics) = build(location, context);
diagnostics.AddRange(buildDiagnostics
.Select(diagnostic => Diagnostics.Generate(context.Symbols.SourceFile, diagnostic, statementPosition)));

return statement;
}

Expand Down Expand Up @@ -1325,6 +1332,12 @@ private static SpecializationImplementation BuildUserDefinedImplementation(
var implementation = BuildScope(root.Children.GetEnumerator(), context, diagnostics);
context.Symbols.EndScope();

// Finalize types.
diagnostics.AddRange(context.Inference.AmbiguousDiagnostics
.Select(diagnostic => Diagnostics.Generate(sourceFile, diagnostic)));
var resolver = InferenceContextModule.Resolver(context.Inference);
implementation = resolver.Statements.OnScope(implementation);

// Verify that all paths return a value if needed (or fail), and that the specialization's required runtime
// capabilities are supported by the execution target.
var (allPathsReturn, returnDiagnostics) = SyntaxProcessing.SyntaxTree.AllPathsReturnValueOrFail(implementation);
Expand Down Expand Up @@ -1470,10 +1483,8 @@ QsSpecialization BuildSpecialization(
{
var specPos = root.Fragment.Range.Start;
var (arg, messages) = buildArg(userDefined.Item);
foreach (var msg in messages)
{
diagnostics.Add(Diagnostics.Generate(spec.Source.AssemblyOrCodeFile, msg, specPos));
}
diagnostics.AddRange(messages.Select(message =>
Diagnostics.Generate(spec.Source.AssemblyOrCodeFile, message, specPos)));

QsGeneratorDirective? GetDirective(QsSpecializationKind k) => definedSpecs.TryGetValue(k, out defined) && defined.Item1.IsValue ? defined.Item1.Item : null;
var requiredFunctorSupport = RequiredFunctorSupport(kind, GetDirective).ToImmutableHashSet();
Expand All @@ -1486,7 +1497,8 @@ QsSpecialization BuildSpecialization(
root, spec.Source.AssemblyOrCodeFile, arg, requiredFunctorSupport, context, diagnostics);
QsCompilerError.Verify(context.Symbols.AllScopesClosed, "all scopes should be closed");
}
implementation = implementation ?? SpecializationImplementation.Intrinsic;

implementation ??= SpecializationImplementation.Intrinsic;
return GetSpecialization(spec, signature, implementation, comments);
}

Expand Down
75 changes: 48 additions & 27 deletions src/QsCompiler/DataStructures/Diagnostics.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,21 +152,30 @@ type ErrorCode =
| ControlledAdjointGenArgMismatch = 4114
| MisplacedDeclarationAttribute = 4115

| MissingExprInArray = 5001
| MultipleTypesInArray = 5002
// TODO: RELEASE 2021-10: Remove MissingExprInArray.
| [<Obsolete "This diagnostic is no longer in use.">] MissingExprInArray = 5001
// TODO: RELEASE 2021-10: Remove MultipleTypesInArray.
| [<Obsolete "This diagnostic is no longer in use.">] MultipleTypesInArray = 5002
| InvalidArrayItemIndex = 5003
| ItemAccessForNonArray = 5004
| InvalidTypeInArithmeticExpr = 5005
| InvalidTypeForConcatenation = 5006
| InvalidTypeInEqualityComparison = 5007
| ArgumentMismatchInBinaryOp = 5008
| TypeMismatchInConditional = 5009
| ExpressionOfUnknownType = 5010
| ExpectingUnitExpr = 5011
| ExpectingIntExpr = 5012
// TODO: RELEASE 2021-10: Remove ArgumentMismatchInBinaryOp.
| [<Obsolete "This diagnostic is no longer in use.">] ArgumentMismatchInBinaryOp = 5008
// TODO: RELEASE 2021-10: Remove TypeMismatchInConditional.
| [<Obsolete "This diagnostic is no longer in use.">] TypeMismatchInConditional = 5009
// TODO: RELEASE 2021-10: Remove ExpressionOfUnknownType.
| [<Obsolete "This diagnostic is no longer in use.">] ExpressionOfUnknownType = 5010
// TODO: RELEASE 2021-10: Remove ExpectingUnitExpr.
| [<Obsolete "This diagnostic is no longer in use.">] ExpectingUnitExpr = 5011
// TODO: RELEASE 2021-10: Remove ExpectingIntExpr.
| [<Obsolete "This diagnostic is no longer in use.">] ExpectingIntExpr = 5012
| ExpectingIntegralExpr = 5013
| ExpectingBoolExpr = 5014
| ExpectingStringExpr = 5015
// TODO: RELEASE 2021-10: Remove ExpectingBoolExpr.
| [<Obsolete "This diagnostic is no longer in use.">] ExpectingBoolExpr = 5014
// TODO: RELEASE 2021-10: Remove ExpectingStringExpr.
| [<Obsolete "This diagnostic is no longer in use.">] ExpectingStringExpr = 5015
| ExpectingUserDefinedType = 5016
| InvalidAdjointApplication = 5017
| InvalidControlledApplication = 5018
Expand Down Expand Up @@ -217,28 +226,40 @@ type ErrorCode =
| InaccessibleTypeInNamespace = 6110
| InaccessibleCallableInNamespace = 6111

| ArgumentTupleShapeMismatch = 6201
| ArgumentTupleMismatch = 6202
// TODO: RELEASE 2021-10: Remove ArgumentTupleShapeMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] ArgumentTupleShapeMismatch = 6201
// TODO: RELEASE 2021-10: Remove ArgumentTupleMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] ArgumentTupleMismatch = 6202
| ArrayBaseTypeMismatch = 6203
| UserDefinedTypeMismatch = 6204
| CallableTypeInputTypeMismatch = 6205
| CallableTypeOutputTypeMismatch = 6206
| MissingFunctorSupport = 6207
| ExcessFunctorSupport = 6208
| FunctorSupportMismatch = 6209
| ArgumentTypeMismatch = 6210
| UnexpectedTupleArgument = 6211
// TODO: RELEASE 2021-10: Remove UserDefinedTypeMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] UserDefinedTypeMismatch = 6204
// TODO: RELEASE 2021-10: Remove CallableTypeInputTypeMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] CallableTypeInputTypeMismatch = 6205
// TODO: RELEASE 2021-10: Remove CallableTypeOutputTypeMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] CallableTypeOutputTypeMismatch = 6206
// TODO: RELEASE 2021-10: Remove MissingFunctorSupport.
| [<Obsolete "This diagnostic is no longer in use.">] MissingFunctorSupport = 6207
// TODO: RELEASE 2021-10: Remove ExcessFunctorSupport.
| [<Obsolete "This diagnostic is no longer in use.">] ExcessFunctorSupport = 6208
// TODO: RELEASE 2021-10: Remove FunctorSupportMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] FunctorSupportMismatch = 6209
// TODO: RELEASE 2021-10: Remove ArgumentTypeMismatch.
| [<Obsolete "This diagnostic is no longer in use.">] ArgumentTypeMismatch = 6210
// TODO: RELEASE 2021-10: Remove UnexpectedTupleArgument.
| [<Obsolete "This diagnostic is no longer in use.">] UnexpectedTupleArgument = 6211
| AmbiguousTypeParameterResolution = 6212
| ConstrainsTypeParameter = 6213
| [<Obsolete("This diagnostic is no longer in use.")>] DirectRecursionWithinTemplate = 6214
// TODO: RELEASE 2021-10: Remove ConstrainsTypeParameter.
| [<Obsolete "This diagnostic is no longer in use.">] ConstrainsTypeParameter = 6213
| GlobalTypeAlreadyExists = 6215
| GlobalCallableAlreadyExists = 6216
| LocalVariableAlreadyExists = 6217
| NamedItemAlreadyExists = 6219
| IdentifierCannotHaveTypeArguments = 6220
| WrongNumberOfTypeArguments = 6221
| InvalidUseOfTypeParameterizedObject = 6222
| PartialApplicationOfTypeParameter = 6223
// TODO: RELEASE 2021-10: Remove InvalidUseOfTypeParameterizedObject.
| [<Obsolete "This diagnostic is no longer in use.">] InvalidUseOfTypeParameterizedObject = 6222
// TODO: RELEASE 2021-10: Remove PartialApplicationOfTypeParameter.
| [<Obsolete "This diagnostic is no longer in use.">] PartialApplicationOfTypeParameter = 6223
| IndirectlyReferencedExpressionType = 6224
| TypeMismatchInCopyAndUpdateExpr = 6225
| InterpolatedStringInAttribute = 6226
Expand All @@ -262,8 +283,10 @@ type ErrorCode =
| ExpectingFullNameAsAttributeArgument = 6244
| AttributeInvalidOnSpecialization = 6245
| AttributeInvalidOnCallable = 6246
| UnresolvedTypeParameterForRecursiveCall = 6247
| TypeParameterResConflictWithTypeArgument = 6248
// TODO: RELEASE 2021-10: Remove UnresolvedTypeParameterForRecursiveCall.
| [<Obsolete "This diagnostic is no longer in use.">] UnresolvedTypeParameterForRecursiveCall = 6247
// TODO: RELEASE 2021-10: Remove TypeParameterResConflictWithTypeArgument.
| [<Obsolete "This diagnostic is no longer in use.">] TypeParameterResConflictWithTypeArgument = 6248
| FullNameConflictsWithNamespace = 6249
| InvalidCyclicTypeParameterResolution = 6250
| InvalidCharacterInInterpolatedArgument = 6251
Expand Down Expand Up @@ -745,8 +768,6 @@ type DiagnosticItem =
| ErrorCode.AmbiguousTypeParameterResolution ->
"The type parameter resolution for the expression is ambiguous. Please provide explicit type arguments, e.g. Op<Int, Double>(arg)."
| ErrorCode.ConstrainsTypeParameter -> "The given expression constrains the type parameter(s) {0}."
| ErrorCode.DirectRecursionWithinTemplate ->
"Direct recursive calls within templates require explicit type arguments. Please provide type arguments, e.g. Op<Int, Double>(arg)."
| ErrorCode.GlobalTypeAlreadyExists -> "A type with the name \"{0}\" already exists."
| ErrorCode.GlobalCallableAlreadyExists -> "A callable with the name \"{0}\" already exists."
| ErrorCode.LocalVariableAlreadyExists -> "A variable with the name \"{0}\" already exists."
Expand Down
55 changes: 30 additions & 25 deletions src/QsCompiler/DataStructures/SyntaxTree.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -600,41 +600,46 @@ type ResolvedInitializer =
{
// the private constructor enforces that the guarantees given for any instance of ResolvedInitializer
// -> the static member New replaces the record constructor
_InitializerKind: QsInitializerKind<ResolvedInitializer, TypedExpression>
_ResolvedType: ResolvedType
kind: QsInitializerKind<ResolvedInitializer, TypedExpression>
resolvedType: ResolvedType
}

interface ITuple

/// Contains the fully resolved Q# initializer.
/// By construction never contains any arity-0 or arity-1 tuple types.
member this.Resolution = this._InitializerKind
member this.Resolution = this.kind

/// the fully resolved Q# type of the initializer.
member this.Type = this._ResolvedType

/// <summary>
/// Builds a ResolvedInitializer based on a compatible Q# initializer kind, and replaces the (inaccessible) record constructor.
/// Replaces an arity-1 tuple by its item type.
/// </summary>
/// <exception cref="ArgumentException">The given type kind is an empty tuple.</exception>
static member New(kind: QsInitializerKind<ResolvedInitializer, TypedExpression>) =
let qArrayT = Qubit |> ResolvedType.New |> ArrayType |> ResolvedType.New
member this.Type = this.resolvedType

let buildTupleType is =
TupleType((is |> Seq.map (fun x -> x._ResolvedType)).ToImmutableArray()) |> ResolvedType.New
module ResolvedInitializer =
let create range kind =
let arrayType = Qubit |> ResolvedType.create range |> ArrayType |> ResolvedType.create range

match kind with
| QsInitializerKind.QubitTupleAllocation is when is.Length = 0 ->
ArgumentException "tuple initializer requires at least one item" |> raise
| QsInitializerKind.QubitTupleAllocation is when is.Length = 1 -> is.[0]
| QsInitializerKind.QubitTupleAllocation is ->
{ _InitializerKind = kind; _ResolvedType = buildTupleType is }
| QsInitializerKind.QubitRegisterAllocation _ -> { _InitializerKind = kind; _ResolvedType = qArrayT }
| QsInitializerKind.SingleQubitAllocation ->
{ _InitializerKind = kind; _ResolvedType = Qubit |> ResolvedType.New }
| QsInitializerKind.InvalidInitializer ->
{ _InitializerKind = kind; _ResolvedType = InvalidType |> ResolvedType.New }
let tupleType =
Seq.map (fun init -> init.resolvedType)
>> ImmutableArray.CreateRange
>> TupleType
>> ResolvedType.create range

match kind with
| QsInitializerKind.QubitTupleAllocation items when items.IsEmpty ->
ArgumentException "Tuple initializer is empty." |> raise
| QsInitializerKind.QubitTupleAllocation items when items.Length = 1 -> items.[0]
| QsInitializerKind.QubitTupleAllocation items -> { kind = kind; resolvedType = tupleType items }
| QsInitializerKind.QubitRegisterAllocation _ -> { kind = kind; resolvedType = arrayType }
| QsInitializerKind.SingleQubitAllocation -> { kind = kind; resolvedType = ResolvedType.create range Qubit }
| QsInitializerKind.InvalidInitializer -> { kind = kind; resolvedType = ResolvedType.create range InvalidType }

type ResolvedInitializer with
/// <summary>
/// Builds a ResolvedInitializer based on a compatible Q# initializer kind, and replaces the (inaccessible) record constructor.
/// Replaces an arity-1 tuple by its item type.
/// </summary>
/// <exception cref="ArgumentException">The given type kind is an empty tuple.</exception>
static member New kind =
ResolvedInitializer.create Generated kind

type LocalVariableDeclaration<'Name> =
{
Expand Down
Loading