Context

(* A context. *)

type context = Formula.formula list;;

let empty ():context = []

(**
    @param c The context to extend.
    @param n The formula to add.
*)
let extend (c:context) (n:Formula.formula):context =
    if (List.exists (fun f -> (Formula.equals n f)) c) then c else n::c

let join (c1:context) (c2:context) =
    List.fold_right (fun f c -> extend c f) c2 c1

let exists (c:context) (f:Formula.formula):bool =
    List.exists (Formula.equals f) c

(**
    @param p The parent context.
    @param c The sub-context.
*)
let subcontext (p:context) (c:context):bool =
    not (List.exists (fun x -> not (exists c x)) p)

let to_string (c:context):string =
    match c with
    | []    -> "[]"
    | f::[] -> "[" ^ (Formula.to_string f) ^ "]"
    | f::l  -> "[" ^ (Formula.to_string f) ^
        (List.fold_right (fun f s -> s ^ ", " ^ Formula.to_string f) l "") ^ "]"