// 基礎編のコードを全部くっつけたコード

// 演習2.1
module TypesAndFuncs

// （int型を用いて）偶数の型
let even = x:int{x % 2 = 0}

// 0以上のint型の2つの値を受け取り，それらの和を返す関数
let addfunc (x:int{x >= 0}) (y:int{y >= 0}) : int = x + y

// （if文を用いて）int型の値を受け取り，0以下の値ならtrueをそれ以外はfalseを返す関数
let is_neg (x:int) : bool 
 = if x < 0 then true
   else false


// コード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!"