Используйте метапрограммирование на F * для синтаксической проверки аргумента функции - PullRequest
Новая
       11

Используйте метапрограммирование на F * для синтаксической проверки аргумента функции

0 голосов
/ 05 февраля 2019

Я хотел бы написать функцию, которая обеспечивает, чтобы ее аргумент синтаксически был константной строкой.Вот что я попробовал: 

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.Есть ли способ сделать то, что я хочу в текущем положении вещей?

1 Ответ

0 голосов
/ 05 июня 2019

Я не знаю, нашли ли вы наконец-то решение, но как насчет неявных мета-аргументов?

Они каким-то образом позволяют запускать код 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
...