diff --git a/guppy/cfg/bb.py b/guppy/cfg/bb.py index f5831dbf..95c9f63a 100644 --- a/guppy/cfg/bb.py +++ b/guppy/cfg/bb.py @@ -46,7 +46,7 @@ class BB(ABC): idx: int # Pointer to the CFG that contains this node - cfg: "BaseCFG[Self]" + containing_cfg: "BaseCFG[Self]" # AST statements contained in this BB statements: list[BBStatement] = field(default_factory=list) diff --git a/guppy/checker/cfg_checker.py b/guppy/checker/cfg_checker.py index 1fbb0521..77f2fa51 100644 --- a/guppy/checker/cfg_checker.py +++ b/guppy/checker/cfg_checker.py @@ -1,3 +1,9 @@ +"""Type checking code for control-flow graphs + +Operates on CFGs produced by the `CFGBuilder`. Produces a `CheckedCFG` consisting of +`CheckedBB`s with inferred type signatures. +""" + import collections from dataclasses import dataclass from typing import Sequence @@ -113,11 +119,12 @@ def check_bb( return_ty: GuppyType, globals: Globals, ) -> CheckedBB: - cfg = bb.cfg + cfg = bb.containing_cfg # For the entry BB we have to separately check that all used variables are # defined. For all other BBs, this will be checked when compiling a predecessor. - if len(bb.predecessors) == 0: + if bb == cfg.entry_bb: + assert len(bb.predecessors) == 0 for x, use in bb.vars.used.items(): if x not in cfg.ass_before[bb] and x not in globals.values: raise GuppyError(f"Variable `{x}` is not defined", use) @@ -211,6 +218,6 @@ def check_rows_match(row1: VarRow, row2: VarRow, bb: BB) -> None: raise GuppyError( f"{ident} can refer to different types: " f"`{v1.ty}` (at {{}}) vs `{v2.ty}` (at {{}})", - bb.cfg.live_before[bb][v1.name].vars.used[v1.name], + bb.containing_cfg.live_before[bb][v1.name].vars.used[v1.name], [v1.defined_at, v2.defined_at], ) diff --git a/guppy/checker/expr_checker.py b/guppy/checker/expr_checker.py index d5985bbc..00c141f8 100644 --- a/guppy/checker/expr_checker.py +++ b/guppy/checker/expr_checker.py @@ -1,3 +1,25 @@ +"""Type checking and synthesizing code for expressions. + +Operates on expressions in a basic block after CFG construction. In particular, we +assume that expressions that involve control flow (i.e. short-circuiting and ternary +expressions) have been removed during CFG construction. + +Furthermore, we assume that assignment expressions with the walrus operator := have +been turned into regular assignments and are no longer present. As a result, expressions +are assumed to be side effect free, in the sense that they do not modify the variables +available in the type checking context. + +We may alter/desugar AST nodes during type checking. In particular, we turn `ast.Name` +nodes into either `LocalName` or `GlobalName` nodes and `ast.Call` nodes are turned into +`LocalCall` or `GlobalCall` nodes. Furthermore, all nodes in the resulting AST are +annotated with their type. + +Expressions can be checked against a given type by the `ExprChecker`, raising an Error +if the expressions doesn't have the expected type. Checking is used for annotated +assignments, return values, and function arguments. Alternatively, the `ExprSynthesizer` +can be used to infer a type for an expression. +""" + import ast from typing import Optional, Union, NoReturn, Any diff --git a/guppy/checker/func_checker.py b/guppy/checker/func_checker.py index eeb55c1b..aa7b9c6c 100644 --- a/guppy/checker/func_checker.py +++ b/guppy/checker/func_checker.py @@ -1,3 +1,10 @@ +"""Type checking code for top-level and nested function definitions. + +For top-level functions, we take the `DefinedFunction` containing the `ast.FunctionDef` +node straight from the Python AST. We build a CFG, check it, and return a +`CheckedFunction` containing a `CheckedCFG` with type annotations. +""" + import ast from dataclasses import dataclass @@ -87,7 +94,7 @@ def check_nested_func_def( cfg = func_def.cfg # Find captured variables - parent_cfg = bb.cfg + parent_cfg = bb.containing_cfg def_ass_before = set(func_ty.arg_names) | ctx.locals.keys() maybe_ass_before = def_ass_before | parent_cfg.maybe_ass_before[bb] cfg.analyze(def_ass_before, maybe_ass_before) diff --git a/guppy/checker/stmt_checker.py b/guppy/checker/stmt_checker.py index 4e9535f7..8d9f87c3 100644 --- a/guppy/checker/stmt_checker.py +++ b/guppy/checker/stmt_checker.py @@ -1,3 +1,13 @@ +"""Type checking code for statements. + +Operates on statements in a basic block after CFG construction. In particular, we +assume that statements involving control flow (i.e. if, while, break, and return +statements) have been removed during CFG construction. + +After checking, we return a desugared statement where all sub-expression have beem type +annotated. +""" + import ast from typing import Sequence @@ -94,7 +104,9 @@ def visit_AugAssign(self, node: ast.AugAssign) -> ast.stmt: def visit_Expr(self, node: ast.Expr) -> ast.stmt: # An expression statement where the return value is discarded - node.value, _ = self._synth_expr(node.value) + node.value, ty = self._synth_expr(node.value) + if ty.linear: + raise GuppyTypeError(f"Value with linear type `{ty}` is not used", node) return node def visit_Return(self, node: ast.Return) -> ast.stmt: diff --git a/tests/error/linear_errors/unused_expr.err b/tests/error/linear_errors/unused_expr.err new file mode 100644 index 00000000..6a0ae95e --- /dev/null +++ b/tests/error/linear_errors/unused_expr.err @@ -0,0 +1,7 @@ +Guppy compilation failed. Error in file $FILE:13 + +11: @guppy(module) +12: def foo(q: Qubit) -> None: +13: h(q) + ^^^^ +GuppyTypeError: Value with linear type `Qubit` is not used diff --git a/tests/error/linear_errors/unused_expr.py b/tests/error/linear_errors/unused_expr.py new file mode 100644 index 00000000..6ad60a82 --- /dev/null +++ b/tests/error/linear_errors/unused_expr.py @@ -0,0 +1,16 @@ +import guppy.prelude.quantum as quantum +from guppy.decorator import guppy +from guppy.module import GuppyModule +from guppy.hugr.tys import Qubit + + +module = GuppyModule("test") +module.load(quantum) + + +@guppy(module) +def foo(q: Qubit) -> None: + h(q) + + +module.compile()