(*========================================================================*)
(*                                                                        *)
(*                ppcmem executable model                                 *)
(*                                                                        *)
(*          Susmit Sarkar, University of Cambridge                        *)
(*          Peter Sewell, University of Cambridge                         *)
(*          Jade Alglave, Oxford University                               *)
(*          Luc Maranget, INRIA Rocquencourt                              *)
(*                                                                        *)
(*  This file is copyright 2010,2011 Institut National de Recherche en    *)
(*  Informatique et en Automatique (INRIA), and Susmit Sarkar, Peter      *)
(*  Sewell, and Jade Alglave.                                             *)
(*                                                                        *)
(*  All rights reserved.                                                  *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*========================================================================*)

(* Help emacs fontification -*-caml-*- *)

(*: \section{Utility Definitions} :*)

(* type unit = | Unit *)

(*: \subsection{Option types} :*)
(*
type 'a option = 
  | Some of 'a
  | None
*)

let set_option_map f xs =
  { match f x with Some y -> y end | forall (x IN xs) | match f x with Some _ ->
true | None -> false end }

let rec opt_map (f:'a -> 'b option) (al : 'a list) : 'b list =
  match al with
  | [] -> []
  | a :: al' ->
      let fal' = opt_map f al' in
      match f a with
      | Some a' -> a' :: fal'
      | None -> fal'
      end
  end

(*: Map-like functions and Sets :*)
let funupd f x y = fun x' -> if x'=x then y else f x'

let set_filter f xs =
  Set.fold
    (fun x k ->
      if f x then Set.add x k else k)
    xs {}

(*: \subsection{Relations} :*)
let domain r = { fst p | forall (p IN r) | true }
let range  r = { snd p | forall (p IN r) | true }

let maximal_elements xs r =
    {x | forall (x IN xs) | (forall (x' IN xs). if (x, x') IN r then (x = x') else true)}

let minimal_elements xs r =
    {x | forall (x IN xs) | (forall (x' IN xs). if (x', x) IN r then (x = x') else true)}


let rec tc r =
  let d = domain r in
  let one_step =
    {(x,z) | forall (x IN d) (z IN d) |
        exist (y IN d). (x,y) IN r && (y,z) IN r} in
  if one_step subset r then r else
  tc (one_step union r)

let rec fix (f : 'a set -> 'a set) (x : 'a set) : 'a set =
   let fx = f x in
   if fx subset x then x
   else fix f (fx union x)

let immediate_predecessors r x =
  { x' | forall (x' IN domain r) | (x',x) IN r }

let down_closure r x =
  fix (fun xs -> 
    {x' | forall (x' IN domain r) | 
    exist (x IN xs). x' IN immediate_predecessors r x })
    ({x})

let is_reflexive r =
  let dr = domain r union range r in
  forall (x IN dr). (x,x) IN r

let is_irreflexive r =
  let dr = domain r union range r in
  forall (x IN dr). not ((x,x) IN r)

let is_transitive r =
  let dr = domain r union range r in
  forall (x IN dr) (y IN dr) (z IN dr).
    if (x,y) IN r && (y,z) IN r 
    then (x,z) IN r
    else true

let is_antisymmetric r =
  let dr = domain r union range r in
  forall (x IN dr) (y IN dr).
    if (x,y) IN r && (y,x) IN r
    then x = y
    else true

let is_strict_order r =
  is_transitive r &&
  is_irreflexive r

let is_order r = 
  is_transitive r &&
  is_antisymmetric r &&
  is_reflexive r

let is_linear_order r =
  let dr = domain r union range r in
  (is_order r) && 
  (forall (x IN dr) (y IN dr). ((x,y) IN r || (y,x) IN r))

let is_strict_linear_order r =
  let dr = domain r union range r in
  (is_strict_order r) && 
  (forall (x IN dr) (y IN dr). ((x = y) || (x,y) IN r || (y,x) IN r))

let restrict r xs =
  set_filter (fun (x,y) -> x IN xs && y IN xs) r

let acyclic r =
  let tcr = tc r in
  is_irreflexive tcr

(*: \subsection{Lists as FIFO's} :*)
let add_event l e =
      List.append l [e]

let add_events l es =
      List.append l es

let rec pos_in' l e acc =
       match l with
       | [] -> None
       | e1::l' -> if e = e1 then Some acc else pos_in' l' e (acc+1)
       end

let pos_in l e =
       pos_in' l e 0


let ordered_before_in l e1 e2 =
       match (pos_in l e1,pos_in l e2) with
       | (Some n1,Some n2) -> n1 < n2
       | _ -> false
       end

(*: \subsection{Comparisons} :*)
type comparison = 
  | Equal
  | Less
  | Greater

let compare_num n1 n2 = 
 if n1 < n2 then Less 
 else if n1 > n2 then Greater
 else Equal

let compare_string (s1 : string) (s2 : string) = 
  (* Warning: not an order, only good for equality testing *)
 if s1 = s2 then Equal else Less

let lexicographic_compare (f : 'a -> 'a -> comparison) (g : 'b -> 'b -> comparison) (x : 'a) (y : 'a) (z : 'b) (w : 'b) : comparison = 
  let c = f x y in
  match c with
  | Equal -> g z w
  | _ -> c
  end