// 演習2.2の参考解答

// コード1: アクセスポリシーのリスト
module ACLs
    // ファイル名の型を定義
    type filename = string 
  
    // ファイル名が"demo/tempfile"であればtrueそれ以外であればfalseを返す関数canWriteを定義
    let canWrite (f:filename) = 
    match f with 
    | "demo/tempfile" -> true
    | _ -> false

    // canWriteまたはファイル名が"demo/README"であればtrueそれ以外であればfalseを返す関数canReadを定義
    let canRead (f:filename) = 
    canWrite f
    || f="demo/README"


// コード2: ファイルアクセスプリミティブ
module FileIO
    // アクセスポリシーモジュールを読込
    open ACLs

    // canRead fがtrueと評価される（＝読み出し可能な）ファイル名fを引数に取り，string型の値（読み出した値）を返す関数readを定義
    assume val read : 
        f:filename{canRead f} -> string
    
    // canWrite fがtrueと評価される（＝書き込み可能な）ファイル名fとstring型の値（書き込む値）を引数に取り，unit型の値を返す関数writeを定義
    assume val write : 
        f:filename{canWrite f} -> string -> unit


// コード3: クライアントコードの例
module ClientCode
    open FileIO
    let passwd = "demo/password"
    let readme = "demo/README"
    let tmp = "demo/tempfile"
    
    let staticChecking () =
        // "demo/tempfile"から読み出した値をv1に，"demo/README"から読み出した値をv2に格納
        let v1 = read tmp in
        let v2 = read readme in

        // "demo/tempfile"に"hello!"を書き込み
        write tmp "hello!"