FStar - Различные результаты в режиме fstar и командной строке - PullRequest
Новая
       11

FStar - Различные результаты в режиме fstar и командной строке

0 голосов
/ 01 января 2019

Я следую учебному пособию для F * https://www.fstar -lang.org / tutorial / , и я установил Emacs с режимом fstar https://github.com/FStarLang/fstar-mode.el в Ubuntu.Я думаю, что я не понимаю, как правильно проверять типы файлов, потому что, когда я делаю это для этого файла из учебника, используя два разных метода: 

module Ex01a

open FStar.Exn
open FStar.All
//safe-read-write


type filename = string

(** [canWrite] is a function specifying whether a file [f] can be written *)
let canWrite (f:filename) = 
  match f with 
    | "demo/tempfile" -> true
    | _ -> false

(** [canRead] is also a function ... *)
let canRead (f:filename) = 
  canWrite f               (* writeable files are also readable *)
  || f="demo/README"       (* and so is demo/README *)


val read  : f:filename{canRead f}  -> ML string
let read f  = FStar.IO.print_string ("Dummy read of file " ^ f ^ "\n"); f

val write : f:filename{canWrite f} -> string -> ML unit
let write f s = FStar.IO.print_string ("Dummy write of string " ^ s ^ " to file " ^ f ^ "\n")


let passwd : filename = "demo/password"
let readme : filename = "demo/README"
let tmp    : filename = "demo/tempfile"


val staticChecking : unit -> ML unit
let staticChecking () =
  let v1 = read tmp in
  let v2 = read readme in
  let v3 = read passwd in
  write tmp "hello!"
  (* ; write passwd "junk" // invalid write , fails type-checking *)


exception InvalidRead
val checkedRead : filename -> ML string
let checkedRead f =
  if canRead f then read f else raise InvalidRead


assume val checkedWrite : filename -> string -> ML unit


let dynamicChecking () =
  let v1 = checkedRead tmp in
  let v2 = checkedRead readme in
  let v3 = checkedRead passwd in (* this raises exception *)
  checkedWrite tmp "hello!";
  checkedWrite passwd "junk" (* this raises exception *)

let main = staticChecking (); dynamicChecking ()

, то в зависимости от использования командной строки или проверки типов Emacs, я получаю два разных результата(соответственно неверно и правильно), как представлено здесь:

enter image description here

где сверху, используя «перезагрузить и проверить тип до точки», он корректно находит ошибку встрока "write password" junk "", в то время как консольная строка внизу утверждает, что все условия проверки успешно выполнены.

Чего мне не хватает?

...