module Demo

open FStar.Exn
open FStar.All
open FStar.Mul

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")

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

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 = if false then read tmp else read passwd in // invalid read, fails type-checking
  write tmp "hello!"
*)

(* ; write passwd "junk" // invalid write , fails type-checking *)

let max x y = if x > y then x else y

let _ = assert (
            forall x y.
                max x y >= x &&
                max x y >= y &&
                (max x y = x) || (max x y = y)
                )

val factorial: x:int{x >= 0} -> Tot int
let rec factorial n =
  if n = 0 then 1 else n * (factorial (n - 1))