在 F* 中使用元编程对函数参数进行语法检查

Question

我想编写一个函数，强制其参数在语法上是一个常量字符串。这是我尝试过的：

module Test

module R = FStar.Reflection

let is_literal (t: R.term) =
  match R.inspect_ln t with
  | R.Tv_Const (R.C_String _) -> true
  | _ -> false

let check_literal (s: string { normalize (is_literal (`s)) }) =
  ()

let test () =
  check_literal ""; // should work
  let s = "" in
  check_literal s // should not work

但是，我很确定静态引号（带有 `）不是我想要的，而是带有 quote 的动态引号。但这会将我的先决条件置于 Tac 效果中。在目前的情况下，有什么办法可以做我想做的事吗？

Answer 1

我不知道你是否最终找到了解决方案，但是隐式元参数呢？

它们以某种方式允许运行 Tac 函数调用时的代码，使 quote 可用。

稍微更改一下代码似乎可行：

module Is_lit

open FStar.Tactics

let is_literal (t: term) =
  match inspect_ln t with
  | Tv_Const (C_String _) -> true
  | _ -> false

let check_literal (s: string)
                  (#[(if (normalize_term (is_literal (quote s)))
                      then exact (`())
                      else fail "not a litteral")
                    ] witness: unit)
                  : unit =
  ()

// success
let _ = check_literal "hey" 

// failure
[@expect_failure]
let _ = let s = "hey" in check_literal s

在 F* 中使用元编程对函数参数进行语法检查

Use meta-programming in F* for a syntactic check on a function argument

fstar