Add a new kind of Witness value that carries an expression (#1324)

This renames `Witness` to `ImplWitness` and adds a new form, `SymbolicWitness`, that holds an expression by which a witness can be computed. A common base class `Witness` is provided.

We form the new kind of witness when evaluation of a witness expression fails because the witness is not in scope, as happens when evaluating a subexpression such as a type expression in isolation, and retry evaluation in the larger context when the interpreter performs type instantiation when running the code.

This allows us to properly handle compile-time evaluation of constructs involving witness table lookups when the witness can be statically determined. The intent is that we will eventually also form symbolic witness table references when impl selection finds a non-final witness, in order to support specialization.

Simplify `NominalClassValue`: it can now always store a witness map rather than either a witness map or a witness-or-witness-expression map.
This commit is contained in:
Richard Smith
2022-06-10 14:16:54 -07:00
committed by GitHub
parent dd6ec2b4cb
commit b74d3f80f1
10 changed files with 228 additions and 138 deletions
@@ -0,0 +1,25 @@
// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
// Exceptions. See /LICENSE for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
// RUN: %{explorer} %s 2>&1 | \
// RUN: %{FileCheck} --match-full-lines --allow-unused-prefixes=false %s
// RUN: %{explorer} --parser_debug --trace_file=- %s 2>&1 | \
// RUN: %{FileCheck} --match-full-lines --allow-unused-prefixes %s
// AUTOUPDATE: %{explorer} %s
// CHECK: result: 0
package ExplorerTest api;
interface X { fn F(); }
impl i32 as X { fn F() {} }
fn G[T:! X](v: T) -> Type {
v.F();
return i32;
}
fn Main() -> i32 {
var v: G(0) = 0;
return v;
}