Unfolding rejects the names of fields

[msaaltink]

I'm not sure why it is not possible to unfold a function defined in a record. For example,

let {{
  type R = {f: [8] -> [8], g: [8] -> [8]}
  r = {f = \x -> x+1, g = \x -> 2*x }:R
  }};

prove_print
  do { unfolding ["r.f"]; w4_unint_z3 ["r"]; }
  {{ \x -> r.f (r.g x) != r.g x }};

results in the error

Could not resolve name: "r.f"

[brianhuffman]

Doing that would require something a little more powerful than what unfolding usually does. The unfolding tactic doesn't even use the saw-core rewriter, so it isn't capable of doing any kind of pattern matching; it merely replaces occurrences of the named constants with their definitions wherever they appear in a term.

If you wanted to be able to replace instances of the pattern r.f with \x -> x+1, we would need to implement that using the saw-core rewriting engine, due to the need to do pattern matching on terms. We actually do have some code in saw-core for taking definitions like t = (a, b) and generating a set of rewrite rules like [t.0 = a, t.1 = b]; currently this functionality is used to implement the add_prelude_defs operation on simpsets.

Probably the best way for us to provide the functionality you want is to expose the rewrite-rule-generating functionality in a more direct way in saw-script. For example, we might introduce a function of type Term -> Theorem where you provide a pattern like {{ r.f }}, and it could return a rewrite rule for unfolding that pattern: r.f = (\x -> x+1). You could then use that rewrite rule with simplify, just like you would with any other rewrite rule. And then you could also define yourself (in saw-script) a function of type [Term] -> ProofScript () that would simplify using the generated rules all in one convenient command.

[msaaltink]

That could be useful. Currently I work around this limitation with rewriting, but that requires repeating the Cryptol text of the definition, which is error prone and irritating to maintain. But in terms of priorities for SAW, this is more of an irritation that a dire need.