Merge branch 'stages/check' into feat/poly

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)

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],
             )

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
 

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)

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:

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

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()