fstar - 在 F* 中使用元编程对函数参数进行语法检查
问题描述
我想编写一个函数,强制它的参数在语法上是一个常量字符串。这是我尝试过的:
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 效应中。在目前的情况下,有什么办法可以做我想做的事吗?
解决方案
我不知道您是否最终找到了解决方案,但是隐式元参数呢?
它们以某种方式允许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
推荐阅读
- java - 如何从 JSP 页面生成 PDF 报告
- assembly - 原始 MS-DOS 源代码中的 DI、EI 和 UP 指令(?)是什么?
- django - 从 django 的 Docker 映像的 collectstatic 部分制作静态文件
- azure-devops-self-hosted-agent - Azure DevOps 代理配置成功连接到服务器,但随后失败并显示“错误 VS30063:您无权访问...”
- python - 关键错误问题,当在lenfuction中输入“aa”时(在书名中)
- java - RestTemplate 似乎保留了 Authorization 标头
- firebase - 为什么 Firebase Artifacts 增加了存储的使用以及如何减少?
- reactjs - 是否可以在另一个回调中调用 useCallback
- android - 防止 BottomSheetDialogFragment 隐藏键盘
- python - Python 记录器配置不会影响导入的模块