Implement a "term model" evaluator.

The basic idea behind this evalutor is to use "normalization by evaluation" techniques to perform principled term reduction using the same simulator infrastructure we already have. The main difference from the concrete simulator is that syntax of terms may also appear among the value forms in the simulator. When these unevaluated "neutral" terms appear, the simulator will reconstruct syntax around them corresponding to the constructs it is attempting to evaluate. The result should be a syntactic term that is evaluated "as far as possible" until it gets stuck on some external variable, opaque term, or other term that is (for whatever reason) not in canonical form.
GaloisInc · Jun 17, 2021 · 9065e59 · 9065e59
1 parent e870373
commit 9065e59
Show file tree

Hide file tree

Showing 2 changed files with 1,063 additions and 0 deletions.
diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal
@@ -76,6 +76,7 @@ library
      Verifier.SAW.SCTypeCheck
      Verifier.SAW.Simulator
      Verifier.SAW.Simulator.Concrete
+     Verifier.SAW.Simulator.TermModel
      Verifier.SAW.Simulator.MonadLazy
      Verifier.SAW.Simulator.Prims
      Verifier.SAW.Simulator.RME