module INTERNALS = struct
  module Exn = struct
    open Prim.Exn

    exception Failure of string
    exception IOError of string 
    exception Blame of string * string
    exception PatternMatch of string * string list

    let failwith (msg: string) =
      raise (Failure msg)

    let tryfun[`a] (thunk: unit -o `a) : exn + `a =
      match tryfun_string thunk with
      | Right a        -> Right[exn,`a] a
      | Left (Left e)  -> Left[exn,`a] e
      | Left (Right s) -> Left[exn,`a] (IOError s)

    let raiseBlame (who: string) (what: string) =
      raise (Blame (who, what))
  end

  local
    module INTERNALS = struct
      module Exn = Exn
    end
  with
    module Contract = struct
      type party = string
      type (`a, `b) coercion = party * party -> `a -> `b
      type `a contract = party * party -> `a -> `a

      (* Flat contracts for unlimited values. *)
      let flat['a] (pred: 'a -> bool) : 'a contract =
        fun (neg: party, pos: party) (a: 'a) ->
          if pred a
            then a
            else Exn.raiseBlame pos "violated contract"

      (* Flat contracts for affine values. *)
      let flatA[`a] (pred: `a -> bool * `a) : `a contract =
        fun (neg: party, pos: party) (a: `a) ->
          match pred a with
          | (true, a)  -> a
          | (false, _) -> Exn.raiseBlame pos "violated contract"

      (* The identity contract. *)
      let any[`a] : `a contract =
        fun (_: party, _: party) (a: `a) -> a

      (* Add domain and codomain contracts to a function. *)
      let func[`q]
              [`a1, `a2] (dom: (`a1, `a2) coercion)
              [`b1, `b2] (cod: (`b1, `b2) coercion)
              : (`a2 -[`q]> `b1, `a1 -[`q]> `b2) coercion =
        fun (neg: party, pos: party) (f: `a2 -[`q]> `b1) ->
          fun (a: `a1) -> cod (neg, pos) (f (dom (pos, neg) a))

      (* Coerce an affine function to an unlimited function, and
         check dynamically that it's applied only once. *)
      let affunc[`a1, `a2] (dom: (`a1, `a2) coercion)
                [`b1, `b2] (cod: (`b1, `b2) coercion)
                : (`a2 -o `b1, `a1 -> `b2) coercion =
        fun (neg: party, pos: party) (f: `a2 -o `b1) ->
          let rf = ref (Some f) in
            fun (a: `a1) ->
              match rf <- None[`a2 -o `b1] with
              | Some f -> cod (neg, pos) (f (dom (pos, neg) a))
              | None   -> Exn.raiseBlame neg "reused one-shot function"

      (* Check that an ostensibly unlimited function is actually
         unlimited. *)
      let unfunc[`a1, `a2] (dom: (`a1, `a2) coercion)
                [`b1, `b2] (cod: (`b1, `b2) coercion)
                : (`a2 -> `b1, `a1 -> `b2) coercion =
        fun (neg: party, pos: party) (f: `a2 -> `b1) ->
          fun (x: `a1) ->
            let x' = dom (pos, neg) x in
            let y  = try f x' with
                     | Exn.Blame(p, "reused one-shot function")
                         -> Exn.raiseBlame pos "raised blame" in 
            cod (neg, pos) y
    end
  end
end

let not (b: bool) = if b then false else true
let (!=)['a] (x: 'a) (y: 'a) = not (x == y)

let flip['a,'b,'c] (f: 'a -> 'b -> 'c) (y: 'b) (x: 'a) = f x y

let (<) (x: int) (y: int) = not (y <= x)
let (>) = flip (<)
let (>=) = flip (<=)
let (>.) = flip (<.)
let (>=.) = flip (<=.)

let null = fun 'a (x : 'a list) ->
  match x with
  | Nil -> true
  | _   -> false
let anull = fun `a (xs : `a list) ->
  match xs with
  | Nil          -> (Nil[`a], true)
  | Cons(x, xs') -> (Cons(x, xs'), false)
let hd = fun 'a (xs : 'a list) ->
  let Cons(x, _) = xs in x
let tl = fun 'a (xs : 'a list) ->
  let Cons(_, xs') = xs in xs'
let foldr =
  let rec foldr `a `b (f : `a -> `b -o `b)
                        (z : `b) |[b](xs : `a list) : `b =
        match xs with
        | Nil -> z
        | Cons(x,xs) -> f x (foldr f z xs)
   in foldr
let foldl =
  let rec foldl `a `b (f : `a -> `b -o `b)
                        (z : `b) |[b](xs : `a list) : `b =
        match xs with
        | Nil -> z
        | Cons(x,xs) -> foldl f (f x z) xs
   in foldl
let map `a `b (f: `a -> `b) (xs: `a list) =
      foldr (fun (x: `a) (xs': `b list) -> Cons (f x, xs')) Nil xs
let filter 'a (f: 'a -> bool) (xs: 'a list) =
      foldr (fun (x: 'a) (xs': 'a list) ->
               if f x then Cons(x, xs') else xs')
            Nil
let mapFilterA `a `b (f: `a -> `b option) (xs: `a list) =
      foldr (fun (x: `a) (xs': `b list) ->
               match f x with
               | Some y -> Cons(y, xs')
               | None   -> xs')
            Nil
let revApp[`c] (xs : `c list) (ys : `c list) =
  let cons (x : `c) (acc : `c list) = Cons (x, acc) in
    foldl cons ys xs
let rev[`b] (xs : `b list) = revApp xs Nil
let append[`a] (xs : `a list) = revApp (rev xs)
let length[`a] (xs : `a list) =
  foldr (fun (x : `a) -> (+) 1) 0 xs
let lengthA[`a] (xs : `a list) =
  let count (x : `a) (n : int, xs' : `a list) =
       (1 + n, Cons (x, xs')) in
    foldr count (0, Nil[`a]) xs

let fst[`a,`b] (x: `a, _: `b) = x
let snd[`a,`b] (_: `a, y: `b) = y

let (=>!) [`a] (x: `a) [`b] (y: `b) = (y, x)

open INTERNALS
open Exn