module INTERNALS = struct
  module PrimTypes = INTERNALS.PrimTypes

  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
    exception UninitializedLetRec of string

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

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

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

  local
    module INTERNALS = struct
      module Exn       = Exn
      module PrimTypes = PrimTypes
    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 (pred: 'a -> bool) : 'a contract =
        λ (neg: party, pos: party) (a: 'a) ->
          if pred a
            then a
            else Exn.raiseBlame pos "violated contract"

      (* Flat contracts for affine values. *)
      let flatA (pred: `a -> bool * `a) : `a contract =
        λ (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 contract =
        λ (_: party, _: party) (a: `a) -> a

      (* Add domain and codomain contracts to a function. *)
      let func
               (dom: (`a1, `a2) coercion)
               (cod: (`b1, `b2) coercion)
              : (`a2 -[`q]> `b1, `a1 -[`q]> `b2) coercion =
        λ (neg: party, pos: party) (f: `a2 -[`q]> `b1) ->
          λ (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 (dom: (`a1, `a2) coercion)
                 (cod: (`b1, `b2) coercion)
                : (`a2 -o `b1, `a1 -> `b2) coercion =
        λ (neg: party, pos: party) (f: `a2 -o `b1) ->
          let rf = ref (Some f) in
            λ (a: `a1) ->
              match rf <- None 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 (dom: (`a1, `a2) coercion)
                 (cod: (`b1, `b2) coercion)
                : (`a2 -> `b1, `a1 -> `b2) coercion =
        λ (neg: party, pos: party) (f: `a2 -> `b1) ->
          λ (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

module Function = struct
  let id x             = x
  let const _ x        = x
  let flip f y x       = f x y
  let curry f x y      = f (x, y)
  let uncurry f (x, y) = f x y
  let compose f g x    = f (g x)
  let ($) f x          = f x

  (* Useful for implicit threading syntax: *)
  let ($>) f x         = ((), f x)
  let ($<) f x         = (f x, ())
end

open Function

module Bool = struct
  let not (b: bool) = if b then false else true
  let (!=) (x: 'a) (y: 'a) = not (x == y)
end

open Bool

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

  type `a × `b = `a * `b
  (* These have too-tight precedences *)
  let (≠)  = (!=)
  let (≤)  = (<=)
  let (≥)  = (>=)
  let (≤.) = (<=.)
  let (≥.) = (>=.)
end

open Int

module List = struct
  let null x =
    match x with
    | [] -> true
    | _  -> false

  let anull xs =
    match xs with
    | []       -> ([], true)
    | x :: xs' -> (x :: xs', false)

  let hd (x :: _) = x

  let tl (_ :: xs) = xs

  let rec foldr f z xs =
    match xs with
    | []      -> z
    | x :: xs -> f x (foldr f z xs)

  let rec foldl f z xs =
    match xs with
    | []      -> z
    | x :: xs -> foldl f (f x z) xs

  let map f = foldr (λ x xs' -> f x :: xs') []

  let filter f xs = foldr (λ x xs' -> if f x then x :: xs' else xs') []

  let mapFilterA f =
        foldr (λ x xs' ->
                 match f x with
                 | Some y -> y :: xs'
                 | None   -> xs')
              []

  let revApp xs ys =
    let cons x acc = x :: acc in
      foldl cons ys xs

  let rev xs = revApp xs []

  let append xs = revApp (rev xs)

  let length = foldr (λ _ -> (+) 1) 0

  let lengthA xs =
    let count x (n, xs') = (1 + n, x :: xs') in
      foldr count (0, []) xs

  let rec openFoldr f z o xs = match xs with
    | #Nil         -> z
    | #Cons(x,xs') -> f x (openFoldr f z o xs')
    | other        -> o other
end

open List

let fst (x, _) = x
let snd (_, y) = y

let (=>!) x y = (y, x)
let (⇒) = (=>!)

let (←) = (<-)
let (⇐) = (<-!)

type (|->)  = type Prim.Row.(|->)
let rowCase = Prim.Row.rowCase

module Exn      = INTERNALS.Exn
module Contract = INTERNALS.Contract
open Exn