metis.ml

(* ========================================================================= *)
(* Metis first-order theorem proving derived rule/tactic for HOL Light.      *)
(*                                                                           *)
(* The original Metis was written by Joe Hurd, and it has been widely used   *)
(* for first-order proofs in HOL4 and Isabelle; see:                         *)
(*                                                                           *)
(*            http://www.gilith.com/research/metis/                          *)
(*                                                                           *)
(* This is a port from SML to OCaml and proof-reconstructing integration     *)
(* with HOL Light, written by Michael Faerber and Cezary Kaliszyk.           *)
(*                                                                           *)
(*                (c) Copyright, Joe Hurd, 2001                              *)
(*             (c) Copyright, Joe Leslie-Hurd, 2004                          *)
(*   (c) Copyright, Michael Faerber and Cezary Kaliszyk, 2014-2018.          *)
(*                                                                           *)
(*            Distributed under the same license as HOL Light.               *)
(* ========================================================================= *)

needs "firstorder.ml";;

let metisverb = ref false;;

module Metis_prover = struct

(* ------------------------------------------------------------------------- *)
(* Convenient utility modules.                                               *)
(* ------------------------------------------------------------------------- *)

module Portable = struct

let pointerEqual (p1, p2) = p1 == p2;;

let randomInt x = Random.int x;;
let randomWord () = Random.bits ();;

let critical x = x;;

end

module Option = struct

let getOpt = function
    (Some s, _) -> s
  | (None, x) -> x;;

let isSome = function
    Some _ -> true
  | None -> false;;

let mapPartial f = function
    None -> None
  | Some x -> f x;;

end

module Order = struct

type order = Less | Equal | Greater;;

let orderOfInt = function
   -1 -> Less
  | 0 -> Equal
  | 1 -> Greater
  | _ -> failwith "orderOfInt"
;;

let intOfOrder = function
    Less -> -1
  | Equal -> 0
  | Greater -> 1
;;

let toCompare f = fun (x, y) -> orderOfInt (f x y);;
let fromCompare f = fun x y -> intOfOrder (f (x, y));;

end

module Int = struct

let toString = string_of_int;;

let compare = Order.toCompare (compare : int -> int -> int);;

let maxInt = Some max_int;;

let div x y = x / y;;

let abs = Pervasives.abs;;

end

module Real = struct

open Order

type real = float;;

let compare = toCompare (compare : float -> float -> int);;

let fromInt = float_of_int;;
let floor x = int_of_float (floor x);;

end

(* ------------------------------------------------------------------------- *)
(* Emulating SML Word type (which is unsigned) and other operations.         *)
(* ------------------------------------------------------------------------- *)

module Word = struct

open Order

type word = int;;
let compare = toCompare (compare: word -> word -> int);;

let shiftLeft (x, y) = x lsl y;;
let shiftRight (x, y) = x lsr y;;

(* This is only the same as the SML version, if there is no overflow *)
let minus (x,y) = x - y;;

let andb (x,y) = x land y;;
let orb  (x,y) = x lor y;;
let xorb (x,y) = x lxor y;;
let notb x = lnot x

let toInt x = x;;
let fromInt x = x;;

end

module Math = struct

let exp = Pervasives.exp;;
let ln = Pervasives.log;;
let sqrt = Pervasives.sqrt;;
let pow (x,y) = x ** y;;

end

module Mlist = struct

let foldl f a l = List.fold_left  (fun acc x -> f (x, acc)) a l;;
let foldr f a l = List.fold_right (fun x acc -> f (x, acc)) l a;;
let nth (l, i) = List.nth l i;;
let null = function
    [] -> true
  | _  -> false
let tabulate (n,f) =
  let rec go i = if i == n then [] else f i :: go (i+1)
  in  go 0
let revAppend (l1, l2) = List.rev_append l1 l2;;
let find p l = try Some (List.find p l) with Not_found -> None;;
let all = List.for_all;;

end

(* ========================================================================= *)
(* ML UTILITY FUNCTIONS                                                      *)
(* ========================================================================= *)

module Useful = struct

open Order

(* ------------------------------------------------------------------------- *)
(* OCaml lists (MF).                                                         *)
(* ------------------------------------------------------------------------- *)

let length = List.length;;
let app = List.iter;;

(* ------------------------------------------------------------------------- *)
(* Characters (MF).                                                          *)
(* ------------------------------------------------------------------------- *)

let isDigit c = '0' <= c && c <= '9'

(* ------------------------------------------------------------------------- *)
(* Exceptions.                                                               *)
(* ------------------------------------------------------------------------- *)

exception Error of string;;

exception Bug of string;;

exception Subscript;;

let total f x = try Some (f x) with Error _ -> None;;

let isSome = function
    (Some _) -> true
  | None -> false
;;

let can f x = isSome (total f x);;

(* ------------------------------------------------------------------------- *)
(* Combinators.                                                              *)
(* ------------------------------------------------------------------------- *)

let cComb f x y = f y x;;

let iComb x = x;;

let kComb x y = x;;

let sComb f g x = f x (g x);;

let wComb f x = f x x;;

let rec funpow n f x = match n with
      0 -> x
    | _ -> funpow (n - 1) f (f x);;

let exp m =
      let rec f x y z = match y with
          0 -> z
        | _ -> f (m (x,x)) (Int.div y 2) (if y mod 2 = 0 then z else m (z,x))
    in
      f
    ;;

(* ------------------------------------------------------------------------- *)
(* Pairs.                                                                    *)
(* ------------------------------------------------------------------------- *)

let pair x y = (x,y);;

let swap (x,y) = (y,x);;

let curry f x y = f (x,y);;

let uncurry f (x,y) = f x y;;

(* ------------------------------------------------------------------------- *)
(* State transformers.                                                       *)
(* ------------------------------------------------------------------------- *)

let return : 'a -> 's -> 'a * 's = pair;;

let bind f (g : 'a -> 's -> 'b * 's) x = uncurry g (f x);;

(*fun mmap f (m : 's -> 'a * 's) = bind m (unit o f);

fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I;

fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;*)

(* ------------------------------------------------------------------------- *)
(* Comparisons.                                                              *)
(* ------------------------------------------------------------------------- *)

let revCompare cmp x_y =
    match cmp x_y with Less -> Greater | Equal -> Equal | Greater -> Less;;

let prodCompare xCmp yCmp ((x1,y1),(x2,y2)) =
    match xCmp (x1,x2) with
      Less -> Less
    | Equal -> yCmp (y1,y2)
    | Greater -> Greater;;

let lexCompare cmp =
      let rec lex = function
          ([],[]) -> Equal
        | ([], _ :: _) -> Less
        | (_ :: _, []) -> Greater
        | (x :: xs, y :: ys) ->
          (match cmp (x,y) with
            Less -> Less
          | Equal -> lex (xs,ys)
          | Greater -> Greater)
    in
      lex
    ;;

let boolCompare = function
    (false,true) -> Less
  | (true,false) -> Greater
  | _ -> Equal;;

(* ------------------------------------------------------------------------- *)
(* Lists.                                                                    *)
(* ------------------------------------------------------------------------- *)

let rec first f = function
    [] -> None
  | (x :: xs) -> (match f x with None -> first f xs | s -> s);;

let rec maps (f : 'a -> 's -> 'b * 's) = function
    [] -> return []
  | (x :: xs) ->
    bind (f x) (fun y -> bind (maps f xs) (fun ys -> return (y :: ys)));;

let zipWith f =
    let rec z l = function
          ([], []) -> l
        | (x :: xs, y :: ys) -> z (f x y :: l) (xs, ys)
        | _ -> raise (Error "zipWith: lists different lengths")
    in
      fun xs -> fun ys -> List.rev (z [] (xs, ys))
    ;;

let zip xs ys = zipWith pair xs ys;;

let unzip ab =
  let inc ((x,y),(xs,ys)) = (x :: xs, y :: ys)
  in Mlist.foldl inc ([],[]) (List.rev ab);;

let enumerate l = fst (maps (fun x m -> ((m, x), m + 1)) l 0);;

let revDivide l =
  let rec revDiv acc = function
      (l, 0) -> (acc,l)
    | ([], _) -> raise Subscript
    | (h :: t, n) -> revDiv (h :: acc) (t, n - 1)
  in fun n -> revDiv [] (l, n);;

let divide l n = let (a,b) = revDivide l n in (List.rev a, b);;

let updateNth (n,x) l =
    let (a,b) = revDivide l n
    in
      match b with [] -> raise Subscript | (_ :: t) -> List.rev_append a (x :: t)
;;

let deleteNth n l =
    let (a,b) = revDivide l n
    in
      match b with [] -> raise Subscript | (_ :: t) -> List.rev_append a t
;;

(* ------------------------------------------------------------------------- *)
(* Sets implemented with lists.                                              *)
(* ------------------------------------------------------------------------- *)

let mem x l = List.mem x l;;

(* ------------------------------------------------------------------------- *)
(* Strings.                                                                  *)
(* ------------------------------------------------------------------------- *)

let mkPrefix p s = p ^ s

let stripSuffix pred s =
  let rec strip pos =
    if pos < 0 then "" else
    if pred (s.[pos]) then strip (pos - 1)
    else String.sub s 0 (pos + 1)
  in strip (String.length s - 1);;

(* ------------------------------------------------------------------------- *)
(* Sorting and searching.                                                    *)
(* ------------------------------------------------------------------------- *)

let sort cmp = List.sort (fromCompare cmp);;

let sortMap f cmp = function
    [] -> []
  | ([_] as l) -> l
  | xs ->
      let ncmp ((m,_),(n,_)) = cmp (m,n)
      in let nxs = List.map (fun x -> (f x, x)) xs
      in let nys = List.sort (fromCompare ncmp) nxs
    in
      List.map snd nys
    ;;

(* ------------------------------------------------------------------------- *)
(* Integers.                                                                 *)
(* ------------------------------------------------------------------------- *)

let rec interval m = function
    0 -> []
  | len -> m :: interval (m + 1) (len - 1);;

let divides = function
    (_, 0) -> true
  | (0, _) -> false
  | (a, b) -> b mod (Int.abs a) = 0;;
let divides = curry divides;;

(* ------------------------------------------------------------------------- *)
(* Useful impure features.                                                   *)
(* ------------------------------------------------------------------------- *)

let generator = ref 0;;

  let newIntThunk () =
      let n = !generator
      in generator := n + 1;
        n
      ;;

  let newIntsThunk k () =
      let
        n = !generator

        in generator := n + k;
          interval n k
      ;;

  let newInt () = newIntThunk ();;

  let newInts k =
      if k <= 0 then []
      else (newIntsThunk k) ();;

end

(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
(* ========================================================================= *)

module Pmap = struct

open Order

(* ------------------------------------------------------------------------- *)
(* Importing useful functionality.                                           *)
(* ------------------------------------------------------------------------- *)

exception Bug = Useful.Bug;;

exception Error = Useful.Error;;

let pointerEqual = Portable.pointerEqual;;

let kComb = Useful.kComb;;

let randomInt = Portable.randomInt;;

let randomWord = Portable.randomWord;;

(* ------------------------------------------------------------------------- *)
(* Converting a comparison function to an equality function.                 *)
(* ------------------------------------------------------------------------- *)

let equalKey compareKey key1 key2 = compareKey (key1,key2) = Equal;;

(* ------------------------------------------------------------------------- *)
(* Priorities.                                                               *)
(* ------------------------------------------------------------------------- *)

type priority = Word.word;;

let randomPriority = randomWord;;

let comparePriority = Word.compare;;

(* ------------------------------------------------------------------------- *)
(* Priority search trees.                                                    *)
(* ------------------------------------------------------------------------- *)

type ('key,'value) tree =
    Empty
  | Tree of ('key,'value) node

and ('key,'value) node =
      {size : int;
       priority : priority;
       left : ('key,'value) tree;
       key : 'key;
       value : 'value;
       right : ('key,'value) tree};;

let lowerPriorityNode node1 node2 =
      let p1 = node1.priority
      and p2 = node2.priority
    in
      comparePriority (p1,p2) = Less
    ;;

(* ------------------------------------------------------------------------- *)
(* Tree debugging functions.                                                 *)
(* ------------------------------------------------------------------------- *)

(*BasicDebug
local
  let checkSizes tree =
      match tree with
        Empty -> 0
      | Tree node ->
        let
          let l = checkSizes node.left
          and r = checkSizes node.right

          let () = if l + 1 + r = node.size then () else raise Bug "wrong size"
        in
          size
        end;;

  let checkSorted compareKey x tree =
      match tree with
        Empty -> x
      | Tree node ->
        let
          let x = checkSorted compareKey x node.left

          let () =
              match x with
                None -> ()
              | Some k ->
                match compareKey (k,node.key) with
                  Less -> ()
                | Equal -> raise Bug "duplicate keys"
                | Greater -> raise Bug "unsorted"

          let x = Some key
        in
          checkSorted compareKey x node.right
        end;;

  let checkPriorities compareKey tree =
      match tree with
        Empty -> None
      | Tree node ->
        let

          let () =
              match checkPriorities compareKey node.left with
                None -> ()
              | Some lnode ->
                if not (lowerPriorityNode node lnode) then ()
                else raise Bug "left child has greater priority"

          let () =
              match checkPriorities compareKey right with
                None -> ()
              | Some rnode ->
                if not (lowerPriorityNode node rnode) then ()
                else raise Bug "right child has greater priority"
        in
          Some node
        end;;
in
  let treeCheckInvariants compareKey tree =
      let
        let _ = checkSizes tree

        let _ = checkSorted compareKey None tree

        let _ = checkPriorities compareKey tree
      in
        tree
      end
      handle Error err -> raise (Bug err);;
end;;
*)

(* ------------------------------------------------------------------------- *)
(* Tree operations.                                                          *)
(* ------------------------------------------------------------------------- *)

let treeNew () = Empty;;

let nodeSize node = node.size;;

let treeSize tree =
    match tree with
      Empty -> 0
    | Tree x -> nodeSize x;;

let mkNode priority left key value right =
      let size = treeSize left + 1 + treeSize right
    in
        {size = size;
         priority = priority;
         left = left;
         key = key;
         value = value;
         right = right}
    ;;

let mkTree priority left key value right =
      let node = mkNode priority left key value right
    in
      Tree node
    ;;

(* ------------------------------------------------------------------------- *)
(* Extracting the left and right spines of a tree.                           *)
(* ------------------------------------------------------------------------- *)

let rec treeLeftSpine acc tree =
    match tree with
      Empty -> acc
    | Tree node -> nodeLeftSpine acc node

and nodeLeftSpine acc node =
      treeLeftSpine (node :: acc) node.left
    ;;

let rec treeRightSpine acc tree =
    match tree with
      Empty -> acc
    | Tree node -> nodeRightSpine acc node

and nodeRightSpine acc node =
      treeRightSpine (node :: acc) node.right
    ;;

(* ------------------------------------------------------------------------- *)
(* Singleton trees.                                                          *)
(* ------------------------------------------------------------------------- *)

let mkNodeSingleton priority key value =
      let size = 1
      and left = Empty
      and right = Empty
    in
        {size = size;
         priority = priority;
         left = left;
         key = key;
         value = value;
         right = right}
    ;;

let nodeSingleton (key,value) =
      let priority = randomPriority ()
    in
      mkNodeSingleton priority key value
    ;;

let treeSingleton key_value =
      let node = nodeSingleton key_value
    in
      Tree node
    ;;

(* ------------------------------------------------------------------------- *)
(* Appending two trees, where every element of the first tree is less than   *)
(* every element of the second tree.                                         *)
(* ------------------------------------------------------------------------- *)

let rec treeAppend tree1 tree2 =
    match tree1 with
      Empty -> tree2
    | Tree node1 ->
      match tree2 with
        Empty -> tree1
      | Tree node2 ->
        if lowerPriorityNode node1 node2 then
          let left = treeAppend tree1 node2.left
          in
            mkTree node1.priority left node2.key node2.value node2.right
        else
          let right = treeAppend node1.right tree2
          in
            mkTree node1.priority node1.left node1.key node1.value right
          ;;

(* ------------------------------------------------------------------------- *)
(* Appending two trees and a node, where every element of the first tree is  *)
(* less than the node, which in turn is less than every element of the       *)
(* second tree.                                                              *)
(* ------------------------------------------------------------------------- *)

let treeCombine left node right =
      let left_node = treeAppend left (Tree node)
    in
      treeAppend left_node right
    ;;

(* ------------------------------------------------------------------------- *)
(* Searching a tree for a value.                                             *)
(* ------------------------------------------------------------------------- *)

let rec treePeek compareKey pkey tree =
    match tree with
      Empty -> None
    | Tree node -> nodePeek compareKey pkey node

and nodePeek compareKey pkey node =
      match compareKey (pkey,node.key) with
        Less -> treePeek compareKey pkey node.left
      | Equal -> Some node.value
      | Greater -> treePeek compareKey pkey node.right
    ;;

(* ------------------------------------------------------------------------- *)
(* Tree paths.                                                               *)
(* ------------------------------------------------------------------------- *)

(* Generating a path by searching a tree for a key/value pair *)

let rec treePeekPath compareKey pkey path tree =
    match tree with
      Empty -> (path,None)
    | Tree node -> nodePeekPath compareKey pkey path node

and nodePeekPath compareKey pkey path node =
      match compareKey (pkey,node.key) with
        Less -> treePeekPath compareKey pkey ((true,node) :: path) node.left
      | Equal -> (path, Some node)
      | Greater -> treePeekPath compareKey pkey ((false,node) :: path) node.right
    ;;

(* A path splits a tree into left/right components *)

let addSidePath ((wentLeft,node),(leftTree,rightTree)) =
      if wentLeft then (leftTree, mkTree node.priority rightTree node.key node.value node.right)
      else (mkTree node.priority node.left node.key node.value leftTree, rightTree)
    ;;

let addSidesPath left_right = Mlist.foldl addSidePath left_right;;

let mkSidesPath path = addSidesPath (Empty,Empty) path;;

(* Updating the subtree at a path *)

  let updateTree ((wentLeft,node),tree) =
        if wentLeft then mkTree node.priority tree node.key node.value node.right
        else mkTree node.priority node.left node.key node.value tree;;
  let updateTreePath tree = Mlist.foldl updateTree tree;;

(* Inserting a new node at a path position *)

let insertNodePath node =
      let rec insert left_right path =
          match path with
            [] ->
              let (left,right) = left_right
            in
              treeCombine left node right
          | ((_,snode) as step) :: rest ->
            if lowerPriorityNode snode node then
                let left_right = addSidePath (step,left_right)
              in
                insert left_right rest
            else
                let (left,right) = left_right

                in let tree = treeCombine left node right
              in
                updateTreePath tree path
    in
      insert (Empty,Empty)
    ;;

(* ------------------------------------------------------------------------- *)
(* Using a key to split a node into three components: the keys comparing     *)
(* less than the supplied key, an optional equal key, and the keys comparing *)
(* greater.                                                                  *)
(* ------------------------------------------------------------------------- *)

let nodePartition compareKey pkey node =
      let (path,pnode) = nodePeekPath compareKey pkey [] node
    in
      match pnode with
        None ->
          let (left,right) = mkSidesPath path
        in
          (left,None,right)
      | Some node ->
        let (left,right) = addSidesPath (node.left,node.right) path
        in
          (left, Some (node.key,node.value), right)
    ;;

(* ------------------------------------------------------------------------- *)
(* Searching a tree for a key/value pair.                                    *)
(* ------------------------------------------------------------------------- *)

let rec treePeekKey compareKey pkey tree =
    match tree with
      Empty -> None
    | Tree node -> nodePeekKey compareKey pkey node

and nodePeekKey compareKey pkey node =
      match compareKey (pkey,node.key) with
        Less -> treePeekKey compareKey pkey node.left
      | Equal -> Some (node.key,node.value)
      | Greater -> treePeekKey compareKey pkey node.right
    ;;

(* ------------------------------------------------------------------------- *)
(* Inserting new key/values into the tree.                                   *)
(* ------------------------------------------------------------------------- *)

let treeInsert compareKey key_value tree =
      let (key,value) = key_value

      in let (path,inode) = treePeekPath compareKey key [] tree
    in
      match inode with
        None ->
          let node = nodeSingleton (key,value)
        in
          insertNodePath node path
      | Some node ->
          updateTreePath (Tree node) path
    ;;

(* ------------------------------------------------------------------------- *)
(* Deleting key/value pairs: it raises an exception if the supplied key is   *)
(* not present.                                                              *)
(* ------------------------------------------------------------------------- *)

let rec treeDelete compareKey dkey tree =
    match tree with
      Empty -> raise (Bug "Map.delete: element not found")
    | Tree node -> nodeDelete compareKey dkey node

and nodeDelete compareKey dkey node =
    let size = node.size in
    let priority = node.priority in
    let left = node.left in
    let key = node.key in
    let value = node.value in
    let right = node.right in
      match compareKey (dkey,key) with
        Less ->
          let size = size - 1
          and left = treeDelete compareKey dkey left

          in let node =
                {size = size;
                 priority = priority;
                 left = left;
                 key = key;
                 value = value;
                 right = right}
        in
          Tree node
      | Equal -> treeAppend left right
      | Greater ->
          let size = size - 1
          and right = treeDelete compareKey dkey right

          in let node =
                {size = size;
                 priority = priority;
                 left = left;
                 key = key;
                 value = value;
                 right = right}
        in
          Tree node
    ;;

(* ------------------------------------------------------------------------- *)
(* Partial map is the basic operation for preserving tree structure.         *)
(* It applies its argument function to the elements *in order*.              *)
(* ------------------------------------------------------------------------- *)

let rec treeMapPartial f tree =
    match tree with
      Empty -> Empty
    | Tree node -> nodeMapPartial f node

and nodeMapPartial f x =
    let priority = x.priority in
    let left = x.left in
    let value = x.value in
    let key = x.key in
    let right = x.right in
      let left = treeMapPartial f left
      and vo = f (key,value)
      and right = treeMapPartial f right
    in
      match vo with
        None -> treeAppend left right
      | Some value -> mkTree priority left key value right
    ;;

(* ------------------------------------------------------------------------- *)
(* Mapping tree values.                                                      *)
(* ------------------------------------------------------------------------- *)

let rec treeMap f tree =
    match tree with
      Empty -> Empty
    | Tree node -> Tree (nodeMap f node)

and nodeMap f node =
    let size = node.size in
    let priority = node.priority in
    let left = node.left in
    let key = node.key in
    let value = node.value in
    let right = node.right in
      let left = treeMap f left
      and value = f (key,value)
      and right = treeMap f right
    in
        {size = size;
         priority = priority;
         left = left;
         key = key;
         value = value;
         right = right}
    ;;

(* ------------------------------------------------------------------------- *)
(* Merge is the basic operation for joining two trees. Note that the merged  *)
(* key is always the one from the second map.                                *)
(* ------------------------------------------------------------------------- *)

let rec treeMerge compareKey f1 f2 fb tree1 tree2 =
    match tree1 with
      Empty -> treeMapPartial f2 tree2
    | Tree node1 ->
      match tree2 with
        Empty -> treeMapPartial f1 tree1
      | Tree node2 -> nodeMerge compareKey f1 f2 fb node1 node2

and nodeMerge compareKey f1 f2 fb node1 node2 =
    let priority = node2.priority in
    let left = node2.left in
    let key = node2.key in
    let value = node2.value in
    let right = node2.right in

      let (l,kvo,r) = nodePartition compareKey key node1

      in let left = treeMerge compareKey f1 f2 fb l left
      and right = treeMerge compareKey f1 f2 fb r right

      in let vo =
          match kvo with
            None -> f2 (key,value)
          | Some kv -> fb (kv,(key,value))
    in
      match vo with
        None -> treeAppend left right
      | Some value ->
          let node = mkNodeSingleton priority key value
        in
          treeCombine left node right
    ;;

(* ------------------------------------------------------------------------- *)
(* A union operation on trees.                                               *)
(* ------------------------------------------------------------------------- *)

let rec treeUnion compareKey f f2 tree1 tree2 =
    match tree1 with
      Empty -> tree2
    | Tree node1 ->
      match tree2 with
        Empty -> tree1
      | Tree node2 -> nodeUnion compareKey f f2 node1 node2

and nodeUnion compareKey f f2 node1 node2 =
    if pointerEqual (node1,node2) then nodeMapPartial f2 node1
    else
        let priority = node2.priority in
        let left = node2.left in
        let key = node2.key in
        let value = node2.value in
        let right = node2.right in

        let (l,kvo,r) = nodePartition compareKey key node1

        in let left = treeUnion compareKey f f2 l left
        and right = treeUnion compareKey f f2 r right

        in let vo =
            match kvo with
              None -> Some value
            | Some kv -> f (kv,(key,value))
      in
        match vo with
          None -> treeAppend left right
        | Some value ->
            let node = mkNodeSingleton priority key value
          in
            treeCombine left node right
      ;;

(* ------------------------------------------------------------------------- *)
(* An intersect operation on trees.                                          *)
(* ------------------------------------------------------------------------- *)

let rec treeIntersect compareKey f t1 t2 =
    match t1 with
      Empty -> Empty
    | Tree n1 ->
      match t2 with
        Empty -> Empty
      | Tree n2 -> nodeIntersect compareKey f n1 n2

and nodeIntersect compareKey f n1 n2 =
      let priority = n2.priority in
      let left = n2.left in
      let key = n2.key in
      let value = n2.value in
      let right = n2.right in

      let (l,kvo,r) = nodePartition compareKey key n1

      in let left = treeIntersect compareKey f l left
      and right = treeIntersect compareKey f r right

      in let vo =
          match kvo with
            None -> None
          | Some kv -> f (kv,(key,value))
    in
      match vo with
        None -> treeAppend left right
      | Some value -> mkTree priority left key value right
    ;;

(* ------------------------------------------------------------------------- *)
(* A union operation on trees which simply chooses the second value.         *)
(* ------------------------------------------------------------------------- *)

let rec treeUnionDomain compareKey tree1 tree2 =
    match tree1 with
      Empty -> tree2
    | Tree node1 ->
      match tree2 with
        Empty -> tree1
      | Tree node2 ->
        if pointerEqual (node1,node2) then tree2
        else nodeUnionDomain compareKey node1 node2

and nodeUnionDomain compareKey node1 node2 =
      let priority = node2.priority in
      let left = node2.left in
      let key = node2.key in
      let value = node2.value in
      let right = node2.right in

      let (l,_,r) = nodePartition compareKey key node1

      in let left = treeUnionDomain compareKey l left
      and right = treeUnionDomain compareKey r right

      in let node = mkNodeSingleton priority key value
    in
      treeCombine left node right
    ;;

(* ------------------------------------------------------------------------- *)
(* An intersect operation on trees which simply chooses the second value.    *)
(* ------------------------------------------------------------------------- *)

let rec treeIntersectDomain compareKey tree1 tree2 =
    match tree1 with
      Empty -> Empty
    | Tree node1 ->
      match tree2 with
        Empty -> Empty
      | Tree node2 ->
        if pointerEqual (node1,node2) then tree2
        else nodeIntersectDomain compareKey node1 node2

and nodeIntersectDomain compareKey node1 node2 =
      let priority = node2.priority in
      let left = node2.left in
      let key = node2.key in
      let value = node2.value in
      let right = node2.right in

      let (l,kvo,r) = nodePartition compareKey key node1

      in let left = treeIntersectDomain compareKey l left
      and right = treeIntersectDomain compareKey r right
    in
      if Option.isSome kvo then mkTree priority left key value right
      else treeAppend left right
    ;;

(* ------------------------------------------------------------------------- *)
(* A difference operation on trees.                                          *)
(* ------------------------------------------------------------------------- *)

let rec treeDifferenceDomain compareKey t1 t2 =
    match t1 with
      Empty -> Empty
    | Tree n1 ->
      match t2 with
        Empty -> t1
      | Tree n2 -> nodeDifferenceDomain compareKey n1 n2

and nodeDifferenceDomain compareKey n1 n2 =
    if pointerEqual (n1,n2) then Empty
    else
        let size = n1.size in
        let priority = n1.priority in
        let left = n1.left in
        let key = n1.key in
        let value = n1.value in
        let right = n1.right in

        let (l,kvo,r) = nodePartition compareKey key n2

        in let left = treeDifferenceDomain compareKey left l
        and right = treeDifferenceDomain compareKey right r
      in
        if Option.isSome kvo then treeAppend left right
        else mkTree priority left key value right
      ;;

(* ------------------------------------------------------------------------- *)
(* A subset operation on trees.                                              *)
(* ------------------------------------------------------------------------- *)

let rec treeSubsetDomain compareKey tree1 tree2 =
    match tree1 with
      Empty -> true
    | Tree node1 ->
      match tree2 with
        Empty -> false
      | Tree node2 -> nodeSubsetDomain compareKey node1 node2

and nodeSubsetDomain compareKey node1 node2 =
    pointerEqual (node1,node2) ||
      let size = node1.size in
      let left = node1.left in
      let key = node1.key in
      let right = node1.right in

      size <= nodeSize node2 &&
        let (l,kvo,r) = nodePartition compareKey key node2
      in
        Option.isSome kvo &&
        treeSubsetDomain compareKey left l &&
        treeSubsetDomain compareKey right r
    ;;

(* ------------------------------------------------------------------------- *)
(* Picking an arbitrary key/value pair from a tree.                          *)
(* ------------------------------------------------------------------------- *)

let rec nodePick node =
      (node.key,node.value)
    ;;

let treePick tree =
    match tree with
      Empty -> raise (Bug "Map.treePick")
    | Tree node -> nodePick node;;

(* ------------------------------------------------------------------------- *)
(* Removing an arbitrary key/value pair from a tree.                         *)
(* ------------------------------------------------------------------------- *)

let rec nodeDeletePick node =
    let left = node.left in
    let key = node.key in
    let value = node.value in
    let right = node.right in
      ((key,value), treeAppend left right)
    ;;

let treeDeletePick tree =
    match tree with
      Empty -> raise (Bug "Map.treeDeletePick")
    | Tree node -> nodeDeletePick node;;

(* ------------------------------------------------------------------------- *)
(* Finding the nth smallest key/value (counting from 0).                     *)
(* ------------------------------------------------------------------------- *)

let rec treeNth n tree =
    match tree with
      Empty -> raise (Bug "Map.treeNth")
    | Tree node -> nodeNth n node

and nodeNth n node =
    let left = node.left in
    let key = node.key in
    let value = node.value in
    let right = node.right in

    let k = treeSize left
    in
      if n = k then (key,value)
      else if n < k then treeNth n left
      else treeNth (n - (k + 1)) right
    ;;

(* ------------------------------------------------------------------------- *)
(* Removing the nth smallest key/value (counting from 0).                    *)
(* ------------------------------------------------------------------------- *)

let rec treeDeleteNth n tree =
    match tree with
      Empty -> raise (Bug "Map.treeDeleteNth")
    | Tree node -> nodeDeleteNth n node

and nodeDeleteNth n node =
    let size = node.size in
    let priority = node.priority in
    let left = node.left in
    let key = node.key in
    let value = node.value in
    let right = node.right in

    let k = treeSize left
    in
      if n = k then ((key,value), treeAppend left right)
      else if n < k then
          let (key_value,left) = treeDeleteNth n left

          in let size = size - 1

          in let node =
                {size = size;
                 priority = priority;
                 left = left;
                 key = key;
                 value = value;
                 right = right}
        in
          (key_value, Tree node)
      else
          let n = n - (k + 1)

          in let (key_value,right) = treeDeleteNth n right

          in let size = size - 1

          in let node =
                {size = size;
                 priority = priority;
                 left = left;
                 key = key;
                 value = value;
                 right = right}
        in
          (key_value, Tree node)
    ;;

(* ------------------------------------------------------------------------- *)
(* Iterators.                                                                *)
(* ------------------------------------------------------------------------- *)

type ('key,'value) iterator =
    Left_to_right_iterator of
      ('key * 'value) * ('key,'value) tree * ('key,'value) node list
  | Right_to_left_iterator of
      ('key * 'value) * ('key,'value) tree * ('key,'value) node list;;

let fromSpineLeftToRightIterator nodes =
    match nodes with
      [] -> None
    | n :: nodes ->
      Some (Left_to_right_iterator ((n.key,n.value),n.right,nodes));;

let fromSpineRightToLeftIterator nodes =
    match nodes with
      [] -> None
    | n :: nodes ->
      Some (Right_to_left_iterator ((n.key,n.value),n.left,nodes));;

let addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);;

let addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);;

let treeMkIterator tree = addLeftToRightIterator [] tree;;

let treeMkRevIterator tree = addRightToLeftIterator [] tree;;

let readIterator iter =
    match iter with
      Left_to_right_iterator (key_value,_,_) -> key_value
    | Right_to_left_iterator (key_value,_,_) -> key_value;;

let advanceIterator iter =
    match iter with
      Left_to_right_iterator (_,tree,nodes) -> addLeftToRightIterator nodes tree
    | Right_to_left_iterator (_,tree,nodes) -> addRightToLeftIterator nodes tree;;

let rec foldIterator f acc io =
    match io with
      None -> acc
    | Some iter ->
        let (key,value) = readIterator iter
      in
        foldIterator f (f (key,value,acc)) (advanceIterator iter)
      ;;

let rec findIterator pred io =
    match io with
      None -> None
    | Some iter ->
        let key_value = readIterator iter
      in
        if pred key_value then Some key_value
        else findIterator pred (advanceIterator iter)
      ;;

let rec firstIterator f io =
    match io with
      None -> None
    | Some iter ->
        let key_value = readIterator iter
      in
        match f key_value with
          None -> firstIterator f (advanceIterator iter)
        | s -> s
      ;;

let rec compareIterator compareKey compareValue io1 io2 =
    match (io1,io2) with
      (None,None) -> Equal
    | (None, Some _) -> Less
    | (Some _, None) -> Greater
    | (Some i1, Some i2) ->
        let (k1,v1) = readIterator i1
        and (k2,v2) = readIterator i2
      in
        match compareKey (k1,k2) with
          Less -> Less
        | Equal ->
          (match compareValue (v1,v2) with
             Less -> Less
           | Equal ->
               let io1 = advanceIterator i1
               and io2 = advanceIterator i2
             in
               compareIterator compareKey compareValue io1 io2
           | Greater -> Greater)
        | Greater -> Greater
      ;;

let rec equalIterator equalKey equalValue io1 io2 =
    match (io1,io2) with
      (None,None) -> true
    | (None, Some _) -> false
    | (Some _, None) -> false
    | (Some i1, Some i2) ->
        let (k1,v1) = readIterator i1
        and (k2,v2) = readIterator i2
      in
        equalKey k1 k2 &&
        equalValue v1 v2 &&
          let io1 = advanceIterator i1
          and io2 = advanceIterator i2
        in
          equalIterator equalKey equalValue io1 io2
      ;;

(* ------------------------------------------------------------------------- *)
(* A type of finite maps.                                                    *)
(* ------------------------------------------------------------------------- *)

type ('key,'value) map =
    Map of ('key * 'key -> order) * ('key,'value) tree;;

(* ------------------------------------------------------------------------- *)
(* Map debugging functions.                                                  *)
(* ------------------------------------------------------------------------- *)

(*BasicDebug
let checkInvariants s m =
    let
      let Map (compareKey,tree) = m

      let _ = treeCheckInvariants compareKey tree
    in
      m
    end
    handle Bug bug -> raise (Bug (s ^ "\n" ^ "Map.checkInvariants: " ^ bug));;
*)

(* ------------------------------------------------------------------------- *)
(* Constructors.                                                             *)
(* ------------------------------------------------------------------------- *)

let newMap compareKey =
      let tree = treeNew ()
    in
      Map (compareKey,tree)
    ;;

let singleton compareKey key_value =
      let tree = treeSingleton key_value
    in
      Map (compareKey,tree)
    ;;

(* ------------------------------------------------------------------------- *)
(* Map size.                                                                 *)
(* ------------------------------------------------------------------------- *)

let size (Map (_,tree)) = treeSize tree;;

let null m = size m = 0;;

(* ------------------------------------------------------------------------- *)
(* Querying.                                                                 *)
(* ------------------------------------------------------------------------- *)

let peekKey (Map (compareKey,tree)) key = treePeekKey compareKey key tree;;

let peek (Map (compareKey,tree)) key = treePeek compareKey key tree;;

let inDomain key m = Option.isSome (peek m key);;

let get m key =
    match peek m key with
      None -> raise (Error "Map.get: element not found")
    | Some value -> value;;

let pick (Map (_,tree)) = treePick tree;;

let nth (Map (_,tree)) n = treeNth n tree;;

let random m =
      let n = size m
    in
      if n = 0 then raise (Bug "Map.random: empty")
      else nth m (randomInt n)
    ;;

(* ------------------------------------------------------------------------- *)
(* Adding.                                                                   *)
(* ------------------------------------------------------------------------- *)

let insert (Map (compareKey,tree)) key_value =
      let tree = treeInsert compareKey key_value tree
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let insert = fun m -> fun kv ->
    checkInvariants "Map.insert: result"
      (insert (checkInvariants "Map.insert: input" m) kv);;
*)

let insertList m =
      let ins (key_value,acc) = insert acc key_value
    in
      Mlist.foldl ins m
    ;;

(* ------------------------------------------------------------------------- *)
(* Removing.                                                                 *)
(* ------------------------------------------------------------------------- *)

let delete (Map (compareKey,tree)) dkey =
      let tree = treeDelete compareKey dkey tree
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let delete = fun m -> fun k ->
    checkInvariants "Map.delete: result"
      (delete (checkInvariants "Map.delete: input" m) k);;
*)

let remove m key = if inDomain key m then delete m key else m;;

let deletePick (Map (compareKey,tree)) =
      let (key_value,tree) = treeDeletePick tree
    in
      (key_value, Map (compareKey,tree))
    ;;

(*BasicDebug
let deletePick = fun m ->
    let
      let (kv,m) = deletePick (checkInvariants "Map.deletePick: input" m)
    in
      (kv, checkInvariants "Map.deletePick: result" m)
    end;;
*)

let deleteNth (Map (compareKey,tree)) n =
      let (key_value,tree) = treeDeleteNth n tree
    in
      (key_value, Map (compareKey,tree))
    ;;

(*BasicDebug
let deleteNth = fun m -> fun n ->
    let
      let (kv,m) = deleteNth (checkInvariants "Map.deleteNth: input" m) n
    in
      (kv, checkInvariants "Map.deleteNth: result" m)
    end;;
*)

let deleteRandom m =
      let n = size m
    in
      if n = 0 then raise (Bug "Map.deleteRandom: empty")
      else deleteNth m (randomInt n)
    ;;

(* ------------------------------------------------------------------------- *)
(* Joining (all join operations prefer keys in the second map).              *)
(* ------------------------------------------------------------------------- *)

let merge (first,second,both) (Map (compareKey,tree1)) (Map (_,tree2)) =
      let tree = treeMerge compareKey first second both tree1 tree2
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let merge = fun f -> fun m1 -> fun m2 ->
    checkInvariants "Map.merge: result"
      (merge f
         (checkInvariants "Map.merge: input 1" m1)
         (checkInvariants "Map.merge: input 2" m2));;
*)

let union f (Map (compareKey,tree1)) (Map (_,tree2)) =
      let f2 kv = f (kv,kv)

      in let tree = treeUnion compareKey f f2 tree1 tree2
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let union = fun f -> fun m1 -> fun m2 ->
    checkInvariants "Map.union: result"
      (union f
         (checkInvariants "Map.union: input 1" m1)
         (checkInvariants "Map.union: input 2" m2));;
*)

let intersect f (Map (compareKey,tree1)) (Map (_,tree2)) =
      let tree = treeIntersect compareKey f tree1 tree2
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let intersect = fun f -> fun m1 -> fun m2 ->
    checkInvariants "Map.intersect: result"
      (intersect f
         (checkInvariants "Map.intersect: input 1" m1)
         (checkInvariants "Map.intersect: input 2" m2));;
*)

(* ------------------------------------------------------------------------- *)
(* Iterators over maps.                                                      *)
(* ------------------------------------------------------------------------- *)

let mkIterator (Map (_,tree)) = treeMkIterator tree;;

let mkRevIterator (Map (_,tree)) = treeMkRevIterator tree;;

(* ------------------------------------------------------------------------- *)
(* Mapping and folding.                                                      *)
(* ------------------------------------------------------------------------- *)

let mapPartial f (Map (compareKey,tree)) =
      let tree = treeMapPartial f tree
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let mapPartial = fun f -> fun m ->
    checkInvariants "Map.mapPartial: result"
      (mapPartial f (checkInvariants "Map.mapPartial: input" m));;
*)

let map f (Map (compareKey,tree)) =
      let tree = treeMap f tree
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let map = fun f -> fun m ->
    checkInvariants "Map.map: result"
      (map f (checkInvariants "Map.map: input" m));;
*)

let transform f = map (fun (_,value) -> f value);;

let filter pred =
      let f ((_,value) as key_value) =
          if pred key_value then Some value else None
    in
      mapPartial f
    ;;

let partition p =
      let np x = not (p x)
    in
      fun m -> (filter p m, filter np m)
    ;;

let foldl f b m = foldIterator f b (mkIterator m);;

let foldr f b m = foldIterator f b (mkRevIterator m);;

let app f m = foldl (fun (key,value,()) -> f (key,value)) () m;;

(* ------------------------------------------------------------------------- *)
(* Searching.                                                                *)
(* ------------------------------------------------------------------------- *)

let findl p m = findIterator p (mkIterator m);;

let findr p m = findIterator p (mkRevIterator m);;

let firstl f m = firstIterator f (mkIterator m);;

let firstr f m = firstIterator f (mkRevIterator m);;

let exists p m = Option.isSome (findl p m);;

let all p =
      let np x = not (p x)
    in
      fun m -> not (exists np m)
    ;;

let count pred =
      let f (k,v,acc) = if pred (k,v) then acc + 1 else acc
    in
      foldl f 0
    ;;

(* ------------------------------------------------------------------------- *)
(* Comparing.                                                                *)
(* ------------------------------------------------------------------------- *)

let compare compareValue (m1,m2) =
    if pointerEqual (m1,m2) then Equal
    else
      match Int.compare (size m1, size m2) with
        Less -> Less
      | Equal ->
          let Map (compareKey,_) = m1

          in let io1 = mkIterator m1
          and io2 = mkIterator m2
        in
          compareIterator compareKey compareValue io1 io2
      | Greater -> Greater;;

let equal equalValue m1 m2 =
    pointerEqual (m1,m2) ||
    (size m1 = size m2 &&
       let Map (compareKey,_) = m1

       in let io1 = mkIterator m1
       and io2 = mkIterator m2
     in
       equalIterator (equalKey compareKey) equalValue io1 io2
     );;

(* ------------------------------------------------------------------------- *)
(* Set operations on the domain.                                             *)
(* ------------------------------------------------------------------------- *)

let unionDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
      let tree = treeUnionDomain compareKey tree1 tree2
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let unionDomain = fun m1 -> fun m2 ->
    checkInvariants "Map.unionDomain: result"
      (unionDomain
         (checkInvariants "Map.unionDomain: input 1" m1)
         (checkInvariants "Map.unionDomain: input 2" m2));;
*)

  let uncurriedUnionDomain (m,acc) = unionDomain acc m;;
  let unionListDomain ms =
      match ms with
        [] -> raise (Bug "Map.unionListDomain: no sets")
      | m :: ms -> Mlist.foldl uncurriedUnionDomain m ms;;

let intersectDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
      let tree = treeIntersectDomain compareKey tree1 tree2
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let intersectDomain = fun m1 -> fun m2 ->
    checkInvariants "Map.intersectDomain: result"
      (intersectDomain
         (checkInvariants "Map.intersectDomain: input 1" m1)
         (checkInvariants "Map.intersectDomain: input 2" m2));;
*)

  let uncurriedIntersectDomain (m,acc) = intersectDomain acc m;;
  let intersectListDomain ms =
      match ms with
        [] -> raise (Bug "Map.intersectListDomain: no sets")
      | m :: ms -> Mlist.foldl uncurriedIntersectDomain m ms;;

let differenceDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
      let tree = treeDifferenceDomain compareKey tree1 tree2
    in
      Map (compareKey,tree)
    ;;

(*BasicDebug
let differenceDomain = fun m1 -> fun m2 ->
    checkInvariants "Map.differenceDomain: result"
      (differenceDomain
         (checkInvariants "Map.differenceDomain: input 1" m1)
         (checkInvariants "Map.differenceDomain: input 2" m2));;
*)

let symmetricDifferenceDomain m1 m2 =
    unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);;

let equalDomain m1 m2 = equal (kComb (kComb true)) m1 m2;;

let subsetDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
    treeSubsetDomain compareKey tree1 tree2;;

let disjointDomain m1 m2 = null (intersectDomain m1 m2);;

(* ------------------------------------------------------------------------- *)
(* Converting to and from lists.                                             *)
(* ------------------------------------------------------------------------- *)

let keys m = foldr (fun (key,_,l) -> key :: l) [] m;;

let values m = foldr (fun (_,value,l) -> value :: l) [] m;;

let toList m = foldr (fun (key,value,l) -> (key,value) :: l) [] m;;

let fromList compareKey l =
      let m = newMap compareKey
    in
      insertList m l
    ;;

(* ------------------------------------------------------------------------- *)
(* Pretty-printing.                                                          *)
(* ------------------------------------------------------------------------- *)

let toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";;

end

(* ------------------------------------------------------------------------- *)
(* More map and set modules to support Metis.                                *)
(* ------------------------------------------------------------------------- *)

(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
(* ========================================================================= *)

module Pset = struct

open Order

(* ------------------------------------------------------------------------- *)
(* A type of finite sets.                                                    *)
(* ------------------------------------------------------------------------- *)

type ('elt,'a) map = ('elt,'a) Pmap.map;;

type 'elt set = Set of ('elt,unit) map;;

(* ------------------------------------------------------------------------- *)
(* Converting to and from maps.                                              *)
(* ------------------------------------------------------------------------- *)

let dest (Set m) = m;;

let mapPartial f =
      let mf (elt,()) = f elt
    in
      fun (Set m) -> Pmap.mapPartial mf m
    ;;

let map f =
      let mf (elt,()) = f elt
    in
      fun (Set m) -> Pmap.map mf m
    ;;

let domain m = Set (Pmap.transform (fun _ -> ()) m);;

(* ------------------------------------------------------------------------- *)
(* Constructors.                                                             *)
(* ------------------------------------------------------------------------- *)

let empty cmp = Set (Pmap.newMap cmp);;

let singleton cmp elt = Set (Pmap.singleton cmp (elt,()));;

(* ------------------------------------------------------------------------- *)
(* Set size.                                                                 *)
(* ------------------------------------------------------------------------- *)

let null (Set m) = Pmap.null m;;

let size (Set m) = Pmap.size m;;

(* ------------------------------------------------------------------------- *)
(* Querying.                                                                 *)
(* ------------------------------------------------------------------------- *)

let peek (Set m) elt =
    match Pmap.peekKey m elt with
      Some (elt,()) -> Some elt
    | None -> None;;

let member elt (Set m) = Pmap.inDomain elt m;;

let pick (Set m) =
      let (elt,_) = Pmap.pick m
    in
      elt
    ;;

let nth (Set m) n =
      let (elt,_) = Pmap.nth m n
    in
      elt
    ;;

let random (Set m) =
      let (elt,_) = Pmap.random m
    in
      elt
    ;;

(* ------------------------------------------------------------------------- *)
(* Adding.                                                                   *)
(* ------------------------------------------------------------------------- *)

let add (Set m) elt =
      let m = Pmap.insert m (elt,())
    in
      Set m
    ;;

  let uncurriedAdd (elt,set) = add set elt;;
  let addList set = Mlist.foldl uncurriedAdd set;;

(* ------------------------------------------------------------------------- *)
(* Removing.                                                                 *)
(* ------------------------------------------------------------------------- *)

let delete (Set m) elt =
      let m = Pmap.delete m elt
    in
      Set m
    ;;

let remove (Set m) elt =
      let m = Pmap.remove m elt
    in
      Set m
    ;;

let deletePick (Set m) =
      let ((elt,()),m) = Pmap.deletePick m
    in
      (elt, Set m)
    ;;

let deleteNth (Set m) n =
      let ((elt,()),m) = Pmap.deleteNth m n
    in
      (elt, Set m)
    ;;

let deleteRandom (Set m) =
      let ((elt,()),m) = Pmap.deleteRandom m
    in
      (elt, Set m)
    ;;

(* ------------------------------------------------------------------------- *)
(* Joining.                                                                  *)
(* ------------------------------------------------------------------------- *)

let union (Set m1) (Set m2) = Set (Pmap.unionDomain m1 m2);;

let unionList sets =
      let ms = List.map dest sets
    in
      Set (Pmap.unionListDomain ms)
    ;;

let intersect (Set m1) (Set m2) = Set (Pmap.intersectDomain m1 m2);;

let intersectList sets =
      let ms = List.map dest sets
    in
      Set (Pmap.intersectListDomain ms)
    ;;

let difference (Set m1) (Set m2) =
    Set (Pmap.differenceDomain m1 m2);;

let symmetricDifference (Set m1) (Set m2) =
    Set (Pmap.symmetricDifferenceDomain m1 m2);;

(* ------------------------------------------------------------------------- *)
(* Pmapping and folding.                                                      *)
(* ------------------------------------------------------------------------- *)

let filter pred =
      let mpred (elt,()) = pred elt
    in
      fun (Set m) -> Set (Pmap.filter mpred m)
    ;;

let partition pred =
      let mpred (elt,()) = pred elt
    in
      fun (Set m) ->
           let (m1,m2) = Pmap.partition mpred m
         in
           (Set m1, Set m2)
    ;;

let app f =
      let mf (elt,()) = f elt
    in
      fun (Set m) -> Pmap.app mf m
    ;;

let foldl f =
      let mf (elt,(),acc) = f (elt,acc)
    in
      fun acc -> fun (Set m) -> Pmap.foldl mf acc m
    ;;

let foldr f =
      let mf (elt,(),acc) = f (elt,acc)
    in
      fun acc -> fun (Set m) -> Pmap.foldr mf acc m
    ;;

(* ------------------------------------------------------------------------- *)
(* Searching.                                                                *)
(* ------------------------------------------------------------------------- *)

let findl p =
      let mp (elt,()) = p elt
    in
      fun (Set m) ->
         match Pmap.findl mp m with
           Some (elt,()) -> Some elt
         | None -> None
    ;;

let findr p =
      let mp (elt,()) = p elt
    in
      fun (Set m) ->
         match Pmap.findr mp m with
           Some (elt,()) -> Some elt
         | None -> None
    ;;

let firstl f =
      let mf (elt,()) = f elt
    in
      fun (Set m) -> Pmap.firstl mf m
    ;;

let firstr f =
      let mf (elt,()) = f elt
    in
      fun (Set m) -> Pmap.firstr mf m
    ;;

let exists p =
      let mp (elt,()) = p elt
    in
      fun (Set m) -> Pmap.exists mp m
    ;;

let all p =
      let mp (elt,()) = p elt
    in
      fun (Set m) -> Pmap.all mp m
    ;;

let count p =
      let mp (elt,()) = p elt
    in
      fun (Set m) -> Pmap.count mp m
    ;;

(* ------------------------------------------------------------------------- *)
(* Comparing.                                                                *)
(* ------------------------------------------------------------------------- *)

let compareValue ((),()) = Equal;;

let equalValue () () = true;;

let compare (Set m1, Set m2) = Pmap.compare compareValue (m1,m2);;

let equal (Set m1) (Set m2) = Pmap.equal equalValue m1 m2;;

let subset (Set m1) (Set m2) = Pmap.subsetDomain m1 m2;;

let disjoint (Set m1) (Set m2) = Pmap.disjointDomain m1 m2;;

(* ------------------------------------------------------------------------- *)
(* Converting to and from lists.                                             *)
(* ------------------------------------------------------------------------- *)

let transform f =
      let inc (x,l) = f x :: l
    in
      foldr inc []
    ;;

let toList (Set m) = Pmap.keys m;;

let fromList cmp elts = addList (empty cmp) elts;;

(* ------------------------------------------------------------------------- *)
(* Pretty-printing.                                                          *)
(* ------------------------------------------------------------------------- *)

let toString set =
    "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";;

(* ------------------------------------------------------------------------- *)
(* Iterators over sets                                                       *)
(* ------------------------------------------------------------------------- *)

type 'elt iterator = ('elt,unit) Pmap.iterator;;

let mkIterator (Set m) = Pmap.mkIterator m;;

let mkRevIterator (Set m) = Pmap.mkRevIterator m;;

let readIterator iter =
      let (elt,()) = Pmap.readIterator iter
    in
      elt
    ;;

let advanceIterator iter = Pmap.advanceIterator iter;;


end

(* ========================================================================= *)
(* More map and set types for Metis.                                         *)
(* ========================================================================= *)

module Mmap = struct

exception Error = Useful.Error;;

module type Ordered =
sig
  type t
  val compare : t -> t -> int
end

module Make (Ord : Ordered) =
struct
  module Ma = Map.Make (Ord)

  type +'a map = 'a Ma.t

  let newMap () = Ma.empty;;
  let null = Ma.is_empty;;
  let singleton (k, x) = Ma.singleton k x;;
  let size = Ma.cardinal;;
  let get m k = try Ma.find k m with Not_found -> raise (Error "Mmap.get: element not found");;
  let peek m k = try Some (Ma.find k m) with Not_found -> None;;
  let insert m (k, v) = Ma.add k v m;;
  let toList = Ma.bindings;;
  let fromList l = List.fold_right (fun (v,tm) -> Ma.add v tm) l Ma.empty;;
  let foldl f b m = List.fold_left (fun s (v, tm) -> f (v, tm, s)) b (Ma.bindings m);;
  let foldr = foldl;;
  let filter f = Ma.filter (fun x y -> f (x, y));;
  let inDomain = Ma.mem;;
  let union f m1 m2 =
    let f' k = function
        (Some x, Some y) -> f ((k, x), (k, y))
      | (Some x, None) -> Some x
      | (None, Some y) -> Some y
      | (None, None) -> None
    in Ma.merge (fun k x y -> f' k (x, y)) m1 m2
  let delete m k = Ma.remove k m
  let mapPartial f m = Ma.fold (fun k x acc -> match f (k, x) with Some y -> Ma.add k y acc | None -> acc) m Ma.empty;;
  let transform = Ma.map;;
  let exists f = Ma.exists (fun k m -> f (k,m));;
end
end


module Intmap = struct

open Order

module Ordered = struct type t = int let compare = compare end

include Mmap.Make (Ordered);;

end

module Stringmap = struct

open Order

module Ordered = struct type t = string let compare = compare end

include Mmap.Make (Ordered);;

end

module Mset = struct

module type Ordered =
sig
  type t
  val compare : t -> t -> int
end

module Make (Ord : Ordered) =
struct
  module Se = Set.Make (Ord)

  type set = Se.t;;
  let compare = Order.toCompare Se.compare;;

  let add s x = Se.add x s;;
  let foldr f a s = Se.fold (fun x acc -> f (x,acc)) s a;;
  let foldl = foldr;;
  let member = Se.mem;;
  let empty = Se.empty;;
  let union = Se.union;;
  let difference = Se.diff;;
  let toList = Se.elements;;
  let singleton = Se.singleton;;
  let null = Se.is_empty;;
  let size = Se.cardinal;;
  let pick = Se.choose;;
  let equal = Se.equal;;
  let exists = Se.exists;;
  let fromList l = List.fold_right Se.add l Se.empty;;
  let delete s x = Se.remove x s;;
  let subset = Se.subset;;
  let intersect = Se.inter;;
  let intersectList = function
      [] -> Se.empty
    | (s::ss) -> List.fold_right Se.inter ss s
  let findl p s =
    let go x = function
        (Some _) as s -> s
      | None -> if p x then Some x else None
    in Se.fold go s None;;
  let firstl f s =
    let go x = function
        (Some _) as s -> s
      | None -> f x
     in Se.fold go s None;;
  let transform f s = Se.fold (fun x acc -> f x :: acc) s []
  let all = Se.for_all;;
  let count p s = Se.fold (fun x c -> if p x then c+1 else c) s 0
end

end


module Intset = struct

open Order

module Ordered = struct type t = int let compare = compare end

include Mset.Make (Ordered);;

end


module Sharing = struct

let map = List.map;;
end

(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML                                                    *)
(* ========================================================================= *)

module Heap = struct

(* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)

open Order

exception Empty;;

type 'a node = Em | Tr of int * 'a * 'a node * 'a node;;

type 'a heap = Heap of ('a * 'a -> order) * int * 'a node;;

let rank = function
    Em -> 0
  | (Tr (r,_,_,_)) -> r;;

let makeT (x,a,b) =
  if rank a >= rank b then Tr (rank b + 1, x, a, b) else Tr (rank a + 1, x, b, a);;

let merge cmp =
      let rec mrg = function
          (h,Em) -> h
        | (Em,h) -> h
        | (Tr (_,x,a1,b1) as h1, (Tr (_,y,a2,b2) as h2)) ->
          match cmp (x,y) with
            Greater -> makeT (y, a2, mrg (h1,b2))
          | _ -> makeT (x, a1, mrg (b1,h2))
    in
      mrg
    ;;

let newHeap cmp = Heap (cmp,0,Em);;

let add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (Tr (1,x,Em,Em), a));;

let size (Heap (_, n, _)) = n;;

let null h = size h = 0;;

let top = function
    (Heap (_,_,Em)) -> raise Empty
  | (Heap (_, _, Tr (_,x,_,_))) -> x;;

let remove = function
    (Heap (_,_,Em)) -> raise Empty
  | (Heap (f, n, Tr (_,x,a,b))) -> (x, Heap (f, n - 1, merge f (a,b)));;

let app f =
      let rec ap = function
          [] -> ()
        | (Em :: rest) -> ap rest
        | (Tr (_,d,a,b) :: rest) -> (f d; ap (a :: b :: rest))
    in
      function Heap (_,_,a) -> ap [a]
    ;;

let rec toList h =
    if null h then []
    else
        let (x,h) = remove h
      in
        x :: toList h
      ;;

let toString h =
    "Heap[" ^ (if null h then "" else Int.toString (size h)) ^ "]";;

end

(* ========================================================================= *)
(* NAMES                                                                     *)
(* ========================================================================= *)

module Name = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* A type of names.                                                          *)
(* ------------------------------------------------------------------------- *)

type name = string;;

(* ------------------------------------------------------------------------- *)
(* A total ordering.                                                         *)
(* ------------------------------------------------------------------------- *)

let compare = Order.toCompare (compare : name -> name -> int);;

let equal n1 n2 = n1 = n2;;

(* ------------------------------------------------------------------------- *)
(* Fresh variables.                                                          *)
(* ------------------------------------------------------------------------- *)

let prefix  = "_";;
let numName i = mkPrefix prefix (Int.toString i);;
let newName () = numName (newInt ());;
let newNames n = List.map numName (newInts n);;

let variantPrime avoid =
    let rec variant n = if avoid n then variant (n ^ "'") else n
    in variant;;

let variantNum avoid n =
  let isDigitOrPrime c = c = '\'' || isDigit c
  in if not (avoid n) then n
      else
        let n = stripSuffix isDigitOrPrime n in
        let rec variant i =
          let n_i = n ^ Int.toString i
          in if avoid n_i then variant (i + 1) else n_i
        in variant 0
;;

(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing.                                              *)
(* ------------------------------------------------------------------------- *)

let toString s : string = s;;

let fromString s : name = s;;

module Ordered =
struct type t = name let compare = Order.fromCompare compare end

module Map = Mmap.Make (Ordered);;
module Set = Mset.Make (Ordered);;

end

(* ========================================================================= *)
(* NAME/ARITY PAIRS                                                          *)
(* ========================================================================= *)

module Name_arity = struct

open Useful;;
open Order

(* ------------------------------------------------------------------------- *)
(* A type of name/arity pairs.                                               *)
(* ------------------------------------------------------------------------- *)

type nameArity = Name.name * int;;

let name ((n,_) : nameArity) = n;;

let arity ((_,i) : nameArity) = i;;

(* ------------------------------------------------------------------------- *)
(* Testing for different arities.                                            *)
(* ------------------------------------------------------------------------- *)

let nary i n_i = arity n_i = i;;

let nullary = nary 0
and unary = nary 1
and binary = nary 2
and ternary = nary 3;;

(* ------------------------------------------------------------------------- *)
(* A total ordering.                                                         *)
(* ------------------------------------------------------------------------- *)

let compare ((n1,i1),(n2,i2)) =
    match Name.compare (n1,n2) with
      Less -> Less
    | Equal -> Int.compare (i1,i2)
    | Greater -> Greater;;

let equal (n1,i1) (n2,i2) = i1 = i2 && Name.equal n1 n2;;


module Ordered =
struct type t = nameArity let compare = fromCompare compare end

module Map = struct
  include Mmap.Make (Ordered)

  let compose m1 m2 =
      let pk ((_,a),n) = peek m2 (n,a)
    in
      mapPartial pk m1
    ;;
end

module Set = struct
  include Mset.Make (Ordered)

  let allNullary = all nullary;
end

end

(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS                                                   *)
(* ========================================================================= *)

module Term = struct

open Useful
open Order

(* ------------------------------------------------------------------------- *)
(* A type of first order logic terms.                                        *)
(* ------------------------------------------------------------------------- *)

type var = Name.name;;

type functionName = Name.name;;

type function_t = functionName * int;;

type const = functionName;;

type term =
    Var of Name.name
  | Fn of (Name.name * term list);;

(* ------------------------------------------------------------------------- *)
(* Constructors and destructors.                                             *)
(* ------------------------------------------------------------------------- *)

(* Variables *)

let destVar = function
    (Var v) -> v
  | (Fn _) -> raise (Error "destVar");;

let isVar = can destVar;;

let equalVar v = function
   (Var v') -> Name.equal v v'
  | _       -> false;;

(* Functions *)

let destFn = function
    (Fn f) -> f
  | (Var _) -> raise (Error "destFn");;

let isFn = can destFn;;

let fnName tm = fst (destFn tm);;

let fnArguments tm = snd (destFn tm);;

let fnArity tm = List.length (fnArguments tm);;

let fnFunction tm = (fnName tm, fnArity tm);;

let functions tm =
  let rec letc fs = function
      [] -> fs
    | (Var _ :: tms) -> letc fs tms
    | (Fn (n,l) :: tms) -> letc (Name_arity.Set.add fs (n, List.length l)) (l @ tms)

  in letc Name_arity.Set.empty [tm];;

let functionNames tm =
  let rec letc fs = function
      [] -> fs
    | (Var _ :: tms) -> letc fs tms
    | (Fn (n,l) :: tms) -> letc (Name.Set.add fs n) (l @ tms)
  in letc Name.Set.empty [tm];;

(* Constants *)

let mkConst c = (Fn (c, []));;

let destConst = function
    (Fn (c, [])) -> c
  | _ -> raise (Error "destConst");;

let isConst = can destConst;;

(* Binary functions *)

let mkBinop f (a,b) = Fn (f,[a;b]);;

let destBinop f = function
  (Fn (x,[a;b])) ->
    if Name.equal x f then (a,b) else raise (Error "Term.destBinop: wrong binop")
  | _ -> raise (Error "Term.destBinop: not a binop");;

let isBinop f = can (destBinop f);;

(* ------------------------------------------------------------------------- *)
(* The size of a term in symbols.                                            *)
(* ------------------------------------------------------------------------- *)

let vAR_SYMBOLS = 1;;

let fN_SYMBOLS = 1;;

let symbols tm =
  let rec sz n = function
      [] -> n
    | (Var _ :: tms) -> sz (n + vAR_SYMBOLS) tms
    | (Fn (letc,args) :: tms) -> sz (n + fN_SYMBOLS) (args @ tms)
  in sz 0 [tm];;

(* ------------------------------------------------------------------------- *)
(* A total comparison function for terms.                                    *)
(* ------------------------------------------------------------------------- *)

let compare (tm1,tm2) =
  let rec cmp = function
      ([], []) -> Equal
    | (tm1 :: tms1, tm2 :: tms2) ->
      let tm1_tm2 = (tm1,tm2)
      in
        if Portable.pointerEqual tm1_tm2 then cmp (tms1, tms2)
        else
          (match tm1_tm2 with
            (Var v1, Var v2) ->
            (match Name.compare (v1,v2) with
               Less -> Less
             | Equal -> cmp (tms1, tms2)
             | Greater -> Greater)
          | (Var _, Fn _) -> Less
          | (Fn _, Var _) -> Greater
          | (Fn (f1,a1), Fn (f2,a2)) ->
            (match Name.compare (f1,f2) with
               Less -> Less
             | Equal ->
               (match Int.compare (List.length a1, List.length a2) with
                  Less -> Less
                | Equal -> cmp (a1 @ tms1, a2 @ tms2)
                | Greater -> Greater)
             | Greater -> Greater))
    | _ -> raise (Bug "Term.compare")
  in cmp ([tm1], [tm2]);;

let equal tm1 tm2 = compare (tm1,tm2) = Equal;;

(* ------------------------------------------------------------------------- *)
(* Subterms.                                                                 *)
(* ------------------------------------------------------------------------- *)

type path = int list;;

let rec subterm' = function
    (tm, []) -> tm
  | (Var _, _ :: _) -> raise (Error "Term.subterm: Var")
  | (Fn (_,tms), h :: t) ->
    if h >= List.length tms then raise (Error "Term.replace: Fn")
    else subterm' (List.nth tms h, t);;
let subterm s t = subterm' (s, t);;

let subterms tm =
  let rec subtms = function
      ([], acc) -> acc
    | ((path,tm) :: rest, acc) ->
        let f (n,arg) = (n :: path, arg)
        and acc = (List.rev path, tm) :: acc
        in match tm with
          Var _ -> subtms (rest, acc)
        | Fn (_,args) -> subtms ((List.map f (enumerate args) @ rest), acc)
  in subtms ([([],tm)], []);;


let rec replace tm = function
    ([],res) -> if equal res tm then tm else res
  | (h :: t, res) ->
    match tm with
      Var _ -> raise (Error "Term.replace: Var")
    | Fn (letc,tms) ->
      if h >= List.length tms then raise (Error "Term.replace: Fn")
      else
        let arg = List.nth tms h in
        let arg' = replace arg (t,res)
        in
          if Portable.pointerEqual (arg',arg) then tm
          else Fn (letc, updateNth (h,arg') tms)
;;

let find pred =
      let rec search = function
          [] -> None
        | ((path,tm) :: rest) ->
          if pred tm then Some (List.rev path)
          else
            match tm with
              Var _ -> search rest
            | Fn (_,a) ->
              let subtms = List.map (fun (i,t) -> (i :: path, t)) (enumerate a)
              in search (subtms @ rest)
    in
      fun tm -> search [([],tm)];;


(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let freeIn v tm =
  let rec free v = function
      [] -> false
    | (Var w :: tms) -> Name.equal v w || free v tms
    | (Fn (_,args) :: tms) -> free v (args @ tms);
  in free v [tm];;

let freeVarsList =
  let rec free vs = function
      [] -> vs
    | (Var v :: tms) -> free (Name.Set.add vs v) tms
    | (Fn (_,args) :: tms) -> free vs (args @ tms);
  in free Name.Set.empty;;

let freeVars tm = freeVarsList [tm];;

(* ------------------------------------------------------------------------- *)
(* Fresh variables.                                                          *)
(* ------------------------------------------------------------------------- *)

let newVar () = Var (Name.newName ());;

let newVars n = List.map (fun x -> Var x) (Name.newNames n);;

let avoid av n = Name.Set.member n av;;
let variantPrime av = Name.variantPrime (avoid av);;
let variantNum av = Name.variantNum (avoid av);;

(* ------------------------------------------------------------------------- *)
(* Special support for terms with type annotations.                          *)
(* ------------------------------------------------------------------------- *)

let hasTypeFunctionName = Name.fromString ":";;

let hasTypeFunction = (hasTypeFunctionName,2);;

let destFnHasType ((f,a) : functionName * term list) =
    if not (Name.equal f hasTypeFunctionName) then
      raise (Error "Term.destFnHasType")
    else
      match a with
        [tm;ty] -> (tm,ty)
      | _ -> raise (Error "Term.destFnHasType");;

let isFnHasType = can destFnHasType;;

let isTypedVar tm =
    match tm with
      Var _ -> true
    | Fn letc ->
      match total destFnHasType letc with
        Some (Var _, _) -> true
      | _ -> false;;

let typedSymbols tm =
  let rec sz n = function
      [] -> n
    | (tm :: tms) ->
      match tm with
        Var _ -> sz (n + 1) tms
      | Fn letc ->
        match total destFnHasType letc with
          Some (tm,_) -> sz n (tm :: tms)
        | None ->
          let (_,a) = letc
          in sz (n + 1) (a @ tms)
  in sz 0 [tm];;

let nonVarTypedSubterms tm =
  let rec subtms = function
      ([], acc) -> acc
    | ((path,tm) :: rest, acc) ->
      (match tm with
        Var _ -> subtms (rest, acc)
      | Fn letc ->
        (match total destFnHasType letc with
          Some (t,_) ->
          (match t with
             Var _ -> subtms (rest, acc)
           | Fn _ ->
             let acc = (List.rev path, tm) :: acc
             and rest = (0 :: path, t) :: rest
             in subtms (rest, acc)
          )
        | None ->
            let f (n,arg) = (n :: path, arg) in
            let (_,args) = letc in
            let acc = (List.rev path, tm) :: acc in
            let rest = List.map f (enumerate args) @ rest
          in
            subtms (rest, acc)))
  in subtms ([([],tm)], []);;

(* ------------------------------------------------------------------------- *)
(* Special support for terms with an explicit function application operator. *)
(* ------------------------------------------------------------------------- *)

let appName = Name.fromString ".";;

let mkFnApp (fTm,aTm) = (appName, [fTm;aTm]);;

let mkApp f_a = Fn (mkFnApp f_a);;

let destFnApp ((f,a) : Name.name * term list) =
    if not (Name.equal f appName) then raise (Error "Term.destFnApp")
    else
      match a with
        [fTm;aTm] -> (fTm,aTm)
      | _ -> raise (Error "Term.destFnApp");;

let isFnApp = can destFnApp;;

let destApp tm =
    match tm with
      Var _ -> raise (Error "Term.destApp")
    | Fn letc -> destFnApp letc;;

let isApp = can destApp;;

let listMkApp (f,l) = List.fold_left (fun acc x -> mkApp (x, acc)) f l;;

let stripApp tm =
  let rec strip tms tm =
      match total destApp tm with
        Some (f,a) -> strip (a :: tms) f
      | None -> (tm,tms)
  in strip [] tm;;

(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing.                                              *)
(* ------------------------------------------------------------------------- *)

let rec toString = function
    Var v -> v
  | Fn (n, []) -> n
  | Fn (n, l) -> n ^ "(" ^ String.concat ", " (List.map toString l) ^ ")";;

module Ordered =
struct type t = term let compare = fromCompare compare end

module Map = Map.Make (Ordered);;

module Set = Set.Make (Ordered);;

end

(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
(* ========================================================================= *)

module Substitute = struct

open Useful

(* ------------------------------------------------------------------------- *)
(* A type of first order logic substitutions.                                *)
(* ------------------------------------------------------------------------- *)

type subst = Subst of Term.term Name.Map.map;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let empty = Subst (Name.Map.newMap ());;

let null (Subst m) = Name.Map.null m;;

let size (Subst m) = Name.Map.size m;;

let peek (Subst m) v = Name.Map.peek m v;;

let insert (Subst m) v_tm = Subst (Name.Map.insert m v_tm);;

let singleton v_tm = insert empty v_tm;;

let toList (Subst m) = Name.Map.toList m;;

let fromList l = Subst (Name.Map.fromList l);;

let foldl f b (Subst m) = Name.Map.foldl f b m;;

let foldr f b (Subst m) = Name.Map.foldr f b m;;


(* ------------------------------------------------------------------------- *)
(* Normalizing removes identity substitutions.                               *)
(* ------------------------------------------------------------------------- *)

let normalize (Subst m as sub) =
  let isNotId (v, tm) = not (Term.equalVar v tm) in
  let m' = Name.Map.filter isNotId m
  in if Name.Map.size m = Name.Map.size m' then sub else Subst m'
;;

(* ------------------------------------------------------------------------- *)
(* Applying a substitution to a first order logic term.                      *)
(* ------------------------------------------------------------------------- *)

let subst sub =
  let rec tmSub = function
        (Term.Var v as tm) ->
          (match peek sub v with
             Some tm' -> if Portable.pointerEqual (tm,tm') then tm else tm'
           | None -> tm)
      | (Term.Fn (f,args) as tm) ->
          let args' = Sharing.map tmSub args
          in
            if Portable.pointerEqual (args,args') then tm
            else Term.Fn (f,args')
    in
      fun tm -> if null sub then tm else tmSub tm
    ;;

(* ------------------------------------------------------------------------- *)
(* Restricting a substitution to a given set of variables.                   *)
(* ------------------------------------------------------------------------- *)

let restrict (Subst m as sub) varSet =
      let isRestrictedVar (v, _) = Name.Set.member v varSet in
      let m' = Name.Map.filter isRestrictedVar m
    in
      if Name.Map.size m = Name.Map.size m' then sub else Subst m'
    ;;

let remove (Subst m as sub) varSet =
      let isRestrictedVar (v, _) = not (Name.Set.member v varSet) in
      let m' = Name.Map.filter isRestrictedVar m
    in
      if Name.Map.size m = Name.Map.size m' then sub else Subst m'
    ;;

(* ------------------------------------------------------------------------- *)
(* Composing two substitutions so that the following identity holds:         *)
(*                                                                           *)
(* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm)                 *)
(* ------------------------------------------------------------------------- *)

let compose (Subst m1 as sub1) sub2 =
      let f (v,tm,s) = insert s (v, subst sub2 tm)
    in
      if null sub2 then sub1 else Name.Map.foldl f sub2 m1
    ;;

(* ------------------------------------------------------------------------- *)
(* Creating the union of two compatible substitutions.                       *)
(* ------------------------------------------------------------------------- *)

let union (Subst m1 as s1) (Subst m2 as s2) =
  let compatible ((_,tm1),(_,tm2)) =
      if Term.equal tm1 tm2 then Some tm1
      else raise (Error "Substitute.union: incompatible")
  in
      if Name.Map.null m1 then s2
      else if Name.Map.null m2 then s1
      else Subst (Name.Map.union compatible m1 m2)
;;

(* ------------------------------------------------------------------------- *)
(* Substitutions can be inverted iff they are renaming substitutions.        *)
(* ------------------------------------------------------------------------- *)

let invert (Subst m) =
  let inv = function
      (v, Term.Var w, s) ->
      if Name.Map.inDomain w s then raise (Error "Substitute.invert: non-injective")
      else Name.Map.insert s (w, Term.Var v)
    | (_, Term.Fn _, _) -> raise (Error "Substitute.invert: non-variable")
  in Subst (Name.Map.foldl inv (Name.Map.newMap ()) m)
;;

let isRenaming = can invert;;

(* ------------------------------------------------------------------------- *)
(* Creating a substitution to freshen variables.                             *)
(* ------------------------------------------------------------------------- *)

let freshVars s =
    let add (v, m) = insert m (v, Term.newVar ())
    in
      Name.Set.foldl add empty s
    ;;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let redexes =
    let add (v,_,s) = Name.Set.add s v
    in
      foldl add Name.Set.empty
    ;;

let residueFreeVars =
    let add (_,t,s) = Name.Set.union s (Term.freeVars t)
    in
      foldl add Name.Set.empty
    ;;

let freeVars =
    let add (v,t,s) = Name.Set.union (Name.Set.add s v) (Term.freeVars t)
    in
      foldl add Name.Set.empty
    ;;

(* ------------------------------------------------------------------------- *)
(* Functions.                                                                *)
(* ------------------------------------------------------------------------- *)

let functions =
    let add (_,t,s) = Name_arity.Set.union s (Term.functions t)
    in
      foldl add Name_arity.Set.empty
    ;;

(* ------------------------------------------------------------------------- *)
(* Matching for first order logic terms.                                     *)
(* ------------------------------------------------------------------------- *)

let matchTerms sub tm1 tm2 =
  let rec matchList sub = function
      [] -> sub
    | ((Term.Var v, tm) :: rest) ->
        let sub =
            match peek sub v with
              None -> insert sub (v,tm)
            | Some tm' ->
              if Term.equal tm tm' then sub
              else raise (Error "Substitute.match: incompatible matches")
      in
        matchList sub rest
    | ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) ->
      if Name.equal f1 f2 && length args1 = length args2 then
        matchList sub (zip args1 args2 @ rest)
      else raise (Error "Substitute.match: different structure")
    | _ -> raise (Error "Substitute.match: functions can't match vars")
  in matchList sub [(tm1,tm2)]
;;

(* ------------------------------------------------------------------------- *)
(* Unification for first order logic terms.                                  *)
(* ------------------------------------------------------------------------- *)

let unify sub tm1 tm2 =
  let rec solve sub = function
      [] -> sub
    | (((tm1,tm2) as tm1_tm2) :: rest) ->
      if Portable.pointerEqual tm1_tm2 then solve sub rest
      else solve' sub (subst sub tm1, subst sub tm2, rest)

  and solve' sub = function
      ((Term.Var v), tm, rest) ->
      if Term.equalVar v tm then solve sub rest
      else if Term.freeIn v tm then raise (Error "Substitute.unify: occurs check")
      else
        (match peek sub v with
           None -> solve (compose sub (singleton (v,tm))) rest
         | Some tm' -> solve' sub (tm', tm, rest))
    | (tm1, ((Term.Var _) as tm2), rest) -> solve' sub (tm2, tm1, rest)
    | (Term.Fn (f1,args1), Term.Fn (f2,args2), rest) ->
      if Name.equal f1 f2 && length args1 = length args2 then
        solve sub (zip args1 args2 @ rest)
      else
        raise (Error "Substitute.unify: different structure")

  in solve sub [(tm1,tm2)];;

end

(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS                                                   *)
(* ========================================================================= *)

module Atom = struct

open Useful
open Order

(* ------------------------------------------------------------------------- *)
(* A type for storing first order logic atoms.                               *)
(* ------------------------------------------------------------------------- *)

type relationName = Name.name;;

type relation = relationName * int;;

type atom = relationName * Term.term list;;

(* ------------------------------------------------------------------------- *)
(* Constructors and destructors.                                             *)
(* ------------------------------------------------------------------------- *)

let name ((rel,_) : atom) = rel;;

let arguments ((_,args) : atom) = args;;

let arity atm = length (arguments atm);;

let relation atm = (name atm, arity atm);;

let functions =
    let f (tm,acc) = Name_arity.Set.union (Term.functions tm) acc
    in
      fun atm -> Mlist.foldl f Name_arity.Set.empty (arguments atm)
    ;;

let functionNames =
    let f (tm,acc) = Name.Set.union (Term.functionNames tm) acc
    in
      fun atm -> Mlist.foldl f Name.Set.empty (arguments atm)
    ;;

(* Binary relations *)

let mkBinop p (a,b) : atom = (p,[a;b]);;

let destBinop p = function
    (x,[a;b]) ->
    if Name.equal x p then (a,b) else raise (Error "Atom.destBinop: wrong binop")
  | _ -> raise (Error "Atom.destBinop: not a binop");;

let isBinop p = can (destBinop p);;

(* ------------------------------------------------------------------------- *)
(* The size of an atom in symbols.                                           *)
(* ------------------------------------------------------------------------- *)

let symbols atm =
    Mlist.foldl (fun (tm,z) -> Term.symbols tm + z) 1 (arguments atm);;

(* ------------------------------------------------------------------------- *)
(* A total comparison function for atoms.                                    *)
(* ------------------------------------------------------------------------- *)

let compare ((p1,tms1),(p2,tms2)) =
    match Name.compare (p1,p2) with
      Less -> Less
    | Equal -> lexCompare Term.compare (tms1,tms2)
    | Greater -> Greater;;

let equal atm1 atm2 = compare (atm1,atm2) = Equal;;

(* ------------------------------------------------------------------------- *)
(* Subterms.                                                                 *)
(* ------------------------------------------------------------------------- *)

let subterm =
  let subterm' = function
    (_, []) -> raise (Bug "Atom.subterm: empty path")
  | ((_,tms), h :: t) ->
    if h >= length tms then raise (Error "Atom.subterm: bad path")
    else Term.subterm (Mlist.nth (tms,h)) t
  in fun x y -> subterm' (x, y)

let subterms ((_,tms) : atom) =
    let f ((n,tm),l) = List.map (fun (p,s) -> (n :: p, s)) (Term.subterms tm) @ l
    in
      Mlist.foldl f [] (enumerate tms)
    ;;

let replace ((rel,tms) as atm) = function
    ([],_) -> raise (Bug "Atom.replace: empty path")
  | (h :: t, res) ->
    if h >= length tms then raise (Error "Atom.replace: bad path")
    else
      let tm = Mlist.nth (tms,h)
      in let tm' = Term.replace tm (t,res)
      in
        if Portable.pointerEqual (tm,tm') then atm
        else (rel, updateNth (h,tm') tms)
      ;;

let find pred =
      let f (i,tm) =
          match Term.find pred tm with
            Some path -> Some (i :: path)
          | None -> None
    in
      fun (_,tms) -> first f (enumerate tms)
    ;;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let freeIn v atm = List.exists (Term.freeIn v) (arguments atm);;

let freeVars =
    let f (tm,acc) = Name.Set.union (Term.freeVars tm) acc
    in
      fun atm -> Mlist.foldl f Name.Set.empty (arguments atm)
    ;;

(* ------------------------------------------------------------------------- *)
(* Substitutions.                                                            *)
(* ------------------------------------------------------------------------- *)

let subst sub ((p,tms) as atm) : atom =
    let tms' = Sharing.map (Substitute.subst sub) tms
    in
      if Portable.pointerEqual (tms',tms) then atm else (p,tms')
    ;;

(* ------------------------------------------------------------------------- *)
(* Matching.                                                                 *)
(* ------------------------------------------------------------------------- *)

let matchAtoms sub (p1,tms1) (p2,tms2) =
  let matchArg ((tm1,tm2),sub) = Substitute.matchTerms sub tm1 tm2 in
        let _ = (Name.equal p1 p2 && length tms1 = length tms2) ||
                raise (Error "Atom.match")
      in
        Mlist.foldl matchArg sub (zip tms1 tms2)
      ;;

(* ------------------------------------------------------------------------- *)
(* Unification.                                                              *)
(* ------------------------------------------------------------------------- *)

let unify sub (p1,tms1) (p2,tms2) =
  let unifyArg ((tm1,tm2),sub) = Substitute.unify sub tm1 tm2 in
        let _ = (Name.equal p1 p2 && length tms1 = length tms2) ||
                raise (Error "Atom.unify")
      in
        Mlist.foldl unifyArg sub (zip tms1 tms2)
      ;;

(* ------------------------------------------------------------------------- *)
(* The equality relation.                                                    *)
(* ------------------------------------------------------------------------- *)

let eqRelationName = Name.fromString "=";;

let eqRelationArity = 2;;

let eqRelation = (eqRelationName,eqRelationArity);;

let mkEq = mkBinop eqRelationName;;

let destEq x = destBinop eqRelationName x;;

let isEq x = isBinop eqRelationName x;;

let mkRefl tm = mkEq (tm,tm);;

let destRefl atm =
    let (l,r) = destEq atm
    in let _ = Term.equal l r || raise (Error "Atom.destRefl")
    in
      l
    ;;

let isRefl x = can destRefl x;;

let sym atm =
    let (l,r) = destEq atm
    in let _ = not (Term.equal l r) || raise (Error "Atom.sym: refl")
    in
      mkEq (r,l)
    ;;

let lhs atm = fst (destEq atm);;

let rhs atm = snd (destEq atm);;

(* ------------------------------------------------------------------------- *)
(* Special support for terms with type annotations.                          *)
(* ------------------------------------------------------------------------- *)

let typedSymbols ((_,tms) : atom) =
    Mlist.foldl (fun (tm,z) -> Term.typedSymbols tm + z) 1 tms;;

let nonVarTypedSubterms (_,tms) =
      let addArg ((n,arg),acc) =
          let addTm ((path,tm),acc) = (n :: path, tm) :: acc
          in
            Mlist.foldl addTm acc (Term.nonVarTypedSubterms arg)
    in
      Mlist.foldl addArg [] (enumerate tms)
    ;;


module Ordered =
struct type t = atom let compare = fromCompare compare end

module Map = Mmap.Make (Ordered);;

module Set = Mset.Make (Ordered);;

end


(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS                                                *)
(* ========================================================================= *)

module Formula = struct

open Useful
open Order

(* ------------------------------------------------------------------------- *)
(* A type of first order logic formulas.                                     *)
(* ------------------------------------------------------------------------- *)

type formula =
    True
  | False
  | Atom of Atom.atom
  | Not of formula
  | And of formula * formula
  | Or of formula * formula
  | Imp of formula * formula
  | Iff of formula * formula
  | Forall of Term.var * formula
  | Exists of Term.var * formula;;

(* ------------------------------------------------------------------------- *)
(* Constructors and destructors.                                             *)
(* ------------------------------------------------------------------------- *)

(* Booleans *)

let mkBoolean = function
    true -> True
  | false -> False;;

let destBoolean =
    function True -> true
  | False -> false
  | _ -> raise (Error "destBoolean");;

let isBoolean = can destBoolean;;

let isTrue fm =
    match fm with
      True -> true
    | _ -> false;;

let isFalse fm =
    match fm with
      False -> true
    | _ -> false;;

(* Functions *)

let functions fm =
  let rec funcs fs = function
      [] -> fs
    | (True :: fms) -> funcs fs fms
    | (False :: fms) -> funcs fs fms
    | (Atom atm :: fms) -> funcs (Name_arity.Set.union (Atom.functions atm) fs) fms
    | (Not p :: fms) -> funcs fs (p :: fms)
    | (And (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Or (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Imp (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Iff (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Forall (_,p) :: fms) -> funcs fs (p :: fms)
    | (Exists (_,p) :: fms) -> funcs fs (p :: fms)
  in
    funcs Name_arity.Set.empty [fm];;

let functionNames fm =
  let rec funcs fs = function
      [] -> fs
    | (True :: fms) -> funcs fs fms
    | (False :: fms) -> funcs fs fms
    | (Atom atm :: fms) -> funcs (Name.Set.union (Atom.functionNames atm) fs) fms
    | (Not p :: fms) -> funcs fs (p :: fms)
    | (And (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Or (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Imp (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Iff (p,q) :: fms) -> funcs fs (p :: q :: fms)
    | (Forall (_,p) :: fms) -> funcs fs (p :: fms)
    | (Exists (_,p) :: fms) -> funcs fs (p :: fms)
  in
    funcs Name.Set.empty [fm];;

(* Relations *)
let relations fm =
  let rec rels fs = function
      [] -> fs
    | (True :: fms) -> rels fs fms
    | (False :: fms) -> rels fs fms
    | (Atom atm :: fms) ->
      rels (Name_arity.Set.add fs (Atom.relation atm)) fms
    | (Not p :: fms) -> rels fs (p :: fms)
    | (And (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Or (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Imp (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Iff (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Forall (_,p) :: fms) -> rels fs (p :: fms)
    | (Exists (_,p) :: fms) -> rels fs (p :: fms)
  in rels Name_arity.Set.empty [fm];;


let relationNames fm =
  let rec rels fs = function
      [] -> fs
    | (True :: fms) -> rels fs fms
    | (False :: fms) -> rels fs fms
    | (Atom atm :: fms) -> rels (Name.Set.add fs (Atom.name atm)) fms
    | (Not p :: fms) -> rels fs (p :: fms)
    | (And (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Or (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Imp (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Iff (p,q) :: fms) -> rels fs (p :: q :: fms)
    | (Forall (_,p) :: fms) -> rels fs (p :: fms)
    | (Exists (_,p) :: fms) -> rels fs (p :: fms)
  in rels Name.Set.empty [fm];;

(* Atoms *)

let destAtom = function
    (Atom atm) -> atm
  | _ -> raise (Error "Formula.destAtom");;

let isAtom = can destAtom;;

(* Negations *)

let destNeg = function
    (Not p) -> p
  | _ -> raise (Error "Formula.destNeg");;

let isNeg = can destNeg;;

let stripNeg =
    let rec strip n = function
          (Not fm) -> strip (n + 1) fm
        | fm -> (n,fm)
    in
      strip 0
    ;;

(* Conjunctions *)

let listMkConj fms =
    match List.rev fms with
      [] -> True
    | fm :: fms -> Mlist.foldl (fun (x, y) -> And (x, y)) fm fms;;

let stripConj =
  let rec strip cs = function
      (And (p,q)) -> strip (p :: cs) q
    | fm -> List.rev (fm :: cs)
  in function
      True -> []
    | fm -> strip [] fm;;

let flattenConj =
      let rec flat acc = function
          [] -> acc
        | (And (p,q) :: fms) -> flat acc (q :: p :: fms)
        | (True :: fms) -> flat acc fms
        | (fm :: fms) -> flat (fm :: acc) fms
    in
      fun fm -> flat [] [fm]
    ;;

(* Disjunctions *)

let listMkDisj fms =
    match List.rev fms with
      [] -> False
    | fm :: fms -> Mlist.foldl (fun (x,y) -> Or (x,y)) fm fms;;

let stripDisj =
  let rec strip cs = function
      (Or (p,q)) -> strip (p :: cs) q
    | fm -> List.rev (fm :: cs)
  in function
      False -> []
    | fm -> strip [] fm;;

let flattenDisj =
      let rec flat acc = function
          [] -> acc
        | (Or (p,q) :: fms) -> flat acc (q :: p :: fms)
        | (False :: fms) -> flat acc fms
        | (fm :: fms) -> flat (fm :: acc) fms
    in
      fun fm -> flat [] [fm]
    ;;

(* Equivalences *)

let listMkEquiv fms =
    match List.rev fms with
      [] -> True
    | fm :: fms -> Mlist.foldl (fun (x,y) -> Iff (x,y)) fm fms;;

let stripEquiv =
  let rec strip cs = function
      (Iff (p,q)) -> strip (p :: cs) q
    | fm -> List.rev (fm :: cs)
  in function
      True -> []
    | fm -> strip [] fm;;

let flattenEquiv =
      let rec flat acc = function
          [] -> acc
        | (Iff (p,q) :: fms) -> flat acc (q :: p :: fms)
        | (True :: fms) -> flat acc fms
        | (fm :: fms) -> flat (fm :: acc) fms
    in
      fun fm -> flat [] [fm]
    ;;

(* Universal quantifiers *)

let destForall = function
    (Forall (v,f)) -> (v,f)
  | _ -> raise (Error "destForall");;

let isForall = can destForall;;

let rec listMkForall = function
    ([],body) -> body
  | (v :: vs, body) -> Forall (v, listMkForall (vs,body));;

let setMkForall (vs,body) = Name.Set.foldr (fun (x,y) -> Forall (x,y)) body vs;;

let stripForall =
  let rec strip vs = function
      (Forall (v,b)) -> strip (v :: vs) b
    | tm -> (List.rev vs, tm)
  in
    strip [];;

(* Existential quantifiers *)

let destExists = function
    (Exists (v,f)) -> (v,f)
  | _ -> raise (Error "destExists");;

let isExists = can destExists;;

let rec listMkExists = function
    ([],body) -> body
  | (v :: vs, body) -> Exists (v, listMkExists (vs,body));;

let setMkExists (vs,body) = Name.Set.foldr (fun (x,y) -> Exists (x,y)) body vs;;

let stripExists =
  let rec strip vs = function
      (Exists (v,b)) -> strip (v :: vs) b
    | tm -> (List.rev vs, tm)
  in
    strip [];;

(* ------------------------------------------------------------------------- *)
(* The size of a formula in symbols.                                         *)
(* ------------------------------------------------------------------------- *)

let symbols fm =
  let rec sz n = function
      [] -> n
    | (True :: fms) -> sz (n + 1) fms
    | (False :: fms) -> sz (n + 1) fms
    | (Atom atm :: fms) -> sz (n + Atom.symbols atm) fms
    | (Not p :: fms) -> sz (n + 1) (p :: fms)
    | (And (p,q) :: fms) -> sz (n + 1) (p :: q :: fms)
    | (Or (p,q) :: fms) -> sz (n + 1) (p :: q :: fms)
    | (Imp (p,q) :: fms) -> sz (n + 1) (p :: q :: fms)
    | (Iff (p,q) :: fms) -> sz (n + 1) (p :: q :: fms)
    | (Forall (_,p) :: fms) -> sz (n + 1) (p :: fms)
    | (Exists (_,p) :: fms) -> sz (n + 1) (p :: fms)
in
  sz 0 [fm];;

(* ------------------------------------------------------------------------- *)
(* A total comparison function for formulas.                                 *)
(* ------------------------------------------------------------------------- *)

let compare fm1_fm2 =
  let rec cmp = function
      [] -> Equal
    | (f1_f2 :: fs) ->
      if Portable.pointerEqual f1_f2 then cmp fs
      else
        match f1_f2 with
          (True,True) -> cmp fs
        | (True,_) -> Less
        | (_,True) -> Greater
        | (False,False) -> cmp fs
        | (False,_) -> Less
        | (_,False) -> Greater
        | (Atom atm1, Atom atm2) ->
          (match Atom.compare (atm1,atm2) with
             Less -> Less
           | Equal -> cmp fs
           | Greater -> Greater)
        | (Atom _, _) -> Less
        | (_, Atom _) -> Greater
        | (Not p1, Not p2) -> cmp ((p1,p2) :: fs)
        | (Not _, _) -> Less
        | (_, Not _) -> Greater
        | (And (p1,q1), And (p2,q2)) -> cmp ((p1,p2) :: (q1,q2) :: fs)
        | (And _, _) -> Less
        | (_, And _) -> Greater
        | (Or (p1,q1), Or (p2,q2)) -> cmp ((p1,p2) :: (q1,q2) :: fs)
        | (Or _, _) -> Less
        | (_, Or _) -> Greater
        | (Imp (p1,q1), Imp (p2,q2)) -> cmp ((p1,p2) :: (q1,q2) :: fs)
        | (Imp _, _) -> Less
        | (_, Imp _) -> Greater
        | (Iff (p1,q1), Iff (p2,q2)) -> cmp ((p1,p2) :: (q1,q2) :: fs)
        | (Iff _, _) -> Less
        | (_, Iff _) -> Greater
        | (Forall (v1,p1), Forall (v2,p2)) ->
          (match Name.compare (v1,v2) with
             Less -> Less
           | Equal -> cmp ((p1,p2) :: fs)
           | Greater -> Greater)
        | (Forall _, Exists _) -> Less
        | (Exists _, Forall _) -> Greater
        | (Exists (v1,p1), Exists (v2,p2)) ->
          (match Name.compare (v1,v2) with
             Less -> Less
           | Equal -> cmp ((p1,p2) :: fs)
           | Greater -> Greater)
in
  cmp [fm1_fm2];;

let equal fm1 fm2 = compare (fm1,fm2) = Equal;;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let freeIn v =
      let rec f = function
          [] -> false
        | (True :: fms) -> f fms
        | (False :: fms) -> f fms
        | (Atom atm :: fms) -> Atom.freeIn v atm || f fms
        | (Not p :: fms) -> f (p :: fms)
        | (And (p,q) :: fms) -> f (p :: q :: fms)
        | (Or (p,q) :: fms) -> f (p :: q :: fms)
        | (Imp (p,q) :: fms) -> f (p :: q :: fms)
        | (Iff (p,q) :: fms) -> f (p :: q :: fms)
        | (Forall (w,p) :: fms) ->
          if Name.equal v w then f fms else f (p :: fms)
        | (Exists (w,p) :: fms) ->
          if Name.equal v w then f fms else f (p :: fms)
    in
      fun fm -> f [fm]
    ;;

let add (fm,vs) =
  let rec fv vs = function
      [] -> vs
    | ((_,True) :: fms) -> fv vs fms
    | ((_,False) :: fms) -> fv vs fms
    | ((bv, Atom atm) :: fms) ->
      fv (Name.Set.union vs (Name.Set.difference (Atom.freeVars atm) bv)) fms
    | ((bv, Not p) :: fms) -> fv vs ((bv,p) :: fms)
    | ((bv, And (p,q)) :: fms) -> fv vs ((bv,p) :: (bv,q) :: fms)
    | ((bv, Or (p,q)) :: fms) -> fv vs ((bv,p) :: (bv,q) :: fms)
    | ((bv, Imp (p,q)) :: fms) -> fv vs ((bv,p) :: (bv,q) :: fms)
    | ((bv, Iff (p,q)) :: fms) -> fv vs ((bv,p) :: (bv,q) :: fms)
    | ((bv, Forall (v,p)) :: fms) -> fv vs ((Name.Set.add bv v, p) :: fms)
    | ((bv, Exists (v,p)) :: fms) -> fv vs ((Name.Set.add bv v, p) :: fms)

   in fv vs [(Name.Set.empty,fm)];;

  let freeVars fm = add (fm,Name.Set.empty);;

  let freeVarsList fms = Mlist.foldl add Name.Set.empty fms;;

let specialize fm = snd (stripForall fm);;

let generalize fm = listMkForall (Name.Set.toList (freeVars fm), fm);;

(* ------------------------------------------------------------------------- *)
(* Substitutions.                                                            *)
(* ------------------------------------------------------------------------- *)

  let rec substCheck sub fm = if Substitute.null sub then fm else substFm sub fm

  and substFm sub fm = match fm with
        True -> fm
      | False -> fm
      | Atom (p,tms) ->
          let tms' = Sharing.map (Substitute.subst sub) tms
        in
          if Portable.pointerEqual (tms,tms') then fm else Atom (p,tms')
      | Not p ->
          let p' = substFm sub p
        in
          if Portable.pointerEqual (p,p') then fm else Not p'
      | And (p,q) -> substConn sub fm (fun (x,y) -> And (x,y)) p q
      | Or (p,q) -> substConn sub fm (fun (x,y) -> Or (x,y)) p q
      | Imp (p,q) -> substConn sub fm (fun (x,y) -> Imp (x,y)) p q
      | Iff (p,q) -> substConn sub fm (fun (x,y) -> Iff (x,y)) p q
      | Forall (v,p) -> substQuant sub fm (fun (x,y) -> Forall (x,y)) v p
      | Exists (v,p) -> substQuant sub fm (fun (x,y) -> Exists (x,y)) v p

  and substConn sub fm conn p q =
        let p' = substFm sub p
        and q' = substFm sub q
      in
        if Portable.pointerEqual (p,p') &&
           Portable.pointerEqual (q,q')
        then fm
        else conn (p',q')

  and substQuant sub fm quant v p =
        let v' =
              let f (w,s) =
                  if Name.equal w v then s
                  else
                    match Substitute.peek sub w with
                      None -> Name.Set.add s w
                    | Some tm -> Name.Set.union s (Term.freeVars tm)

              in let vars = freeVars p
              in let vars = Name.Set.foldl f Name.Set.empty vars
            in
              Term.variantPrime vars v

        in let sub =
            if Name.equal v v' then Substitute.remove sub (Name.Set.singleton v)
            else Substitute.insert sub (v, Term.Var v')

        in let p' = substCheck sub p
      in
        if Name.equal v v' && Portable.pointerEqual (p,p') then fm
        else quant (v',p');;

  let subst = substCheck;;

(* ------------------------------------------------------------------------- *)
(* The equality relation.                                                    *)
(* ------------------------------------------------------------------------- *)

let mkEq a_b = Atom (Atom.mkEq a_b);;

let destEq fm = Atom.destEq (destAtom fm);;

let isEq = can destEq;;

let mkNeq a_b = Not (mkEq a_b);;

let destNeq = function
    (Not fm) -> destEq fm
  | _ -> raise (Error "Formula.destNeq");;

let isNeq = can destNeq;;

let mkRefl tm = Atom (Atom.mkRefl tm);;

let destRefl fm = Atom.destRefl (destAtom fm);;

let isRefl = can destRefl;;

let sym fm = Atom (Atom.sym (destAtom fm));;

let lhs fm = fst (destEq fm);;

let rhs fm = snd (destEq fm);;

(* ------------------------------------------------------------------------- *)
(* Parsing and pretty-printing.                                              *)
(* ------------------------------------------------------------------------- *)

let truthName = Name.fromString "T"
and falsityName = Name.fromString "F"
and conjunctionName = Name.fromString "/\\"
and disjunctionName = Name.fromString "\\/"
and implicationName = Name.fromString "==>"
and equivalenceName = Name.fromString "<=>"
and universalName = Name.fromString "!"
and existentialName = Name.fromString "?";;

  let rec demote = function
      True -> Term.Fn (truthName,[])
    | False -> Term.Fn (falsityName,[])
    | (Atom (p,tms)) -> Term.Fn (p,tms)
    | (Not p) ->
      let
        s = "~"
      in
        Term.Fn (Name.fromString s, [demote p])
    | (And (p,q)) -> Term.Fn (conjunctionName, [demote p; demote q])
    | (Or (p,q)) -> Term.Fn (disjunctionName, [demote p; demote q])
    | (Imp (p,q)) -> Term.Fn (implicationName, [demote p; demote q])
    | (Iff (p,q)) -> Term.Fn (equivalenceName, [demote p; demote q])
    | (Forall (v,b)) -> Term.Fn (universalName, [Term.Var v; demote b])
    | (Exists (v,b)) ->
      Term.Fn (existentialName, [Term.Var v; demote b]);;

  let toString fm = Term.toString (demote fm);;


(* ------------------------------------------------------------------------- *)
(* Splitting goals.                                                          *)
(* ------------------------------------------------------------------------- *)

  let add_asms asms goal =
      if Mlist.null asms then goal else Imp (listMkConj (List.rev asms), goal);;

  let add_var_asms asms v goal = add_asms asms (Forall (v,goal));;

  let rec split asms pol fm =
      match (pol,fm) with
        (* Positive splittables *)
        (true,True) -> []
      | (true, Not f) -> split asms false f
      | (true, And (f1,f2)) -> split asms true f1 @ split (f1 :: asms) true f2
      | (true, Or (f1,f2)) -> split (Not f1 :: asms) true f2
      | (true, Imp (f1,f2)) -> split (f1 :: asms) true f2
      | (true, Iff (f1,f2)) ->
        split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
      | (true, Forall (v,f)) -> List.map (add_var_asms asms v) (split [] true f)
        (* Negative splittables *)
      | (false,False) -> []
      | (false, Not f) -> split asms true f
      | (false, And (f1,f2)) -> split (f1 :: asms) false f2
      | (false, Or (f1,f2)) ->
        split asms false f1 @ split (Not f1 :: asms) false f2
      | (false, Imp (f1,f2)) -> split asms true f1 @ split (f1 :: asms) false f2
      | (false, Iff (f1,f2)) ->
        split (f1 :: asms) false f2 @ split (Not f2 :: asms) true f1
      | (false, Exists (v,f)) -> List.map (add_var_asms asms v) (split [] false f)
        (* Unsplittables *)
      | _ -> [add_asms asms (if pol then fm else Not fm)];;

  let splitGoal fm = split [] true fm;;

(*MetisTrace3
let splitGoal = fun fm =>
    let
      let result = splitGoal fm
      let () = Print.trace pp "Formula.splitGoal: fm" fm
      let () = Print.trace (Print.ppList pp) "Formula.splitGoal: result" result
    in
      result
    end;;
*)

module Ordered =
struct type t = formula let compare = fromCompare compare end

module Map = Mmap.Make (Ordered);;

module Set = Mset.Make (Ordered);;

end


(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS                                                *)
(* ========================================================================= *)

module Literal = struct

open Useful;;
open Order

(* ------------------------------------------------------------------------- *)
(* A type for storing first order logic literals.                            *)
(* ------------------------------------------------------------------------- *)

type polarity = bool;;

type literal = polarity * Atom.atom;;

(* ------------------------------------------------------------------------- *)
(* Constructors and destructors.                                             *)
(* ------------------------------------------------------------------------- *)

let polarity ((pol,_) : literal) = pol;;

let atom ((_,atm) : literal) = atm;;

let name lit = Atom.name (atom lit);;

let arguments lit = Atom.arguments (atom lit);;

let arity lit = Atom.arity (atom lit);;

let positive lit = polarity lit;;

let negative lit = not (polarity lit);;

let negate (pol,atm) : literal = (not pol, atm)

let relation lit = Atom.relation (atom lit);;

let functions lit = Atom.functions (atom lit);;

let functionNames lit = Atom.functionNames (atom lit);;

(* Binary relations *)

let mkBinop rel (pol,a,b) : literal = (pol, Atom.mkBinop rel (a,b));;

let destBinop rel ((pol,atm) : literal) =
    match Atom.destBinop rel atm with (a,b) -> (pol,a,b);;

let isBinop rel = can (destBinop rel);;

(* Formulas *)

let toFormula = function
    (true,atm) -> Formula.Atom atm
  | (false,atm) -> Formula.Not (Formula.Atom atm);;

let fromFormula = function
    (Formula.Atom atm) -> (true,atm)
  | (Formula.Not (Formula.Atom atm)) -> (false,atm)
  | _ -> raise (Error "Literal.fromFormula");;

(* ------------------------------------------------------------------------- *)
(* The size of a literal in symbols.                                         *)
(* ------------------------------------------------------------------------- *)

let symbols ((_,atm) : literal) = Atom.symbols atm;;

(* ------------------------------------------------------------------------- *)
(* A total comparison function for literals.                                 *)
(* ------------------------------------------------------------------------- *)

let compare = prodCompare boolCompare Atom.compare;;

let equal (p1,atm1) (p2,atm2) = p1 = p2 && Atom.equal atm1 atm2;;

(* ------------------------------------------------------------------------- *)
(* Subterms.                                                                 *)
(* ------------------------------------------------------------------------- *)

let subterm lit path = Atom.subterm (atom lit) path;;

let subterms lit = Atom.subterms (atom lit);;

let replace ((pol,atm) as lit) path_tm =
      let atm' = Atom.replace atm path_tm
    in
      if Portable.pointerEqual (atm,atm') then lit else (pol,atm')
    ;;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let freeIn v lit = Atom.freeIn v (atom lit);;

let freeVars lit = Atom.freeVars (atom lit);;

(* ------------------------------------------------------------------------- *)
(* Substitutions.                                                            *)
(* ------------------------------------------------------------------------- *)

let subst sub ((pol,atm) as lit) : literal =
      let atm' = Atom.subst sub atm
    in
      if Portable.pointerEqual (atm',atm) then lit else (pol,atm')
    ;;

(* ------------------------------------------------------------------------- *)
(* Matching.                                                                 *)
(* ------------------------------------------------------------------------- *)

let matchLiterals sub ((pol1,atm1) : literal) (pol2,atm2) =
      let _ = pol1 = pol2 || raise (Error "Literal.match")
    in
      Atom.matchAtoms sub atm1 atm2
    ;;

(* ------------------------------------------------------------------------- *)
(* Unification.                                                              *)
(* ------------------------------------------------------------------------- *)

let unify sub ((pol1,atm1) : literal) (pol2,atm2) =
      let _ = pol1 = pol2 || raise (Error "Literal.unify")
    in
      Atom.unify sub atm1 atm2
    ;;

(* ------------------------------------------------------------------------- *)
(* The equality relation.                                                    *)
(* ------------------------------------------------------------------------- *)

let mkEq l_r : literal = (true, Atom.mkEq l_r);;

let destEq = function
    ((true,atm) : literal) -> Atom.destEq atm
  | (false,_) -> raise (Error "Literal.destEq");;

let isEq = can destEq;;

let mkNeq l_r : literal = (false, Atom.mkEq l_r);;

let destNeq = function
    ((false,atm) : literal) -> Atom.destEq atm
  | (true,_) -> raise (Error "Literal.destNeq");;

let isNeq = can destNeq;;

let mkRefl tm = (true, Atom.mkRefl tm);;

let destRefl = function
    (true,atm) -> Atom.destRefl atm
  | (false,_) -> raise (Error "Literal.destRefl");;

let isRefl = can destRefl;;

let mkIrrefl tm = (false, Atom.mkRefl tm);;

let destIrrefl = function
    (true,_) -> raise (Error "Literal.destIrrefl")
  | (false,atm) -> Atom.destRefl atm;;

let isIrrefl = can destIrrefl;;

let sym (pol,atm) : literal = (pol, Atom.sym atm);;

let lhs ((_,atm) : literal) = Atom.lhs atm;;

let rhs ((_,atm) : literal) = Atom.rhs atm;;

(* ------------------------------------------------------------------------- *)
(* Special support for terms with type annotations.                          *)
(* ------------------------------------------------------------------------- *)

let typedSymbols ((_,atm) : literal) = Atom.typedSymbols atm;;

let nonVarTypedSubterms ((_,atm) : literal) = Atom.nonVarTypedSubterms atm;;

(* ------------------------------------------------------------------------- *)
(* Parsing and pretty-printing.                                              *)
(* ------------------------------------------------------------------------- *)

let toString literal = Formula.toString (toFormula literal);;


module Ordered =
struct type t = literal let compare = fromCompare compare end

module Map = Mmap.Make (Ordered);;

module Set =
struct
  include Mset.Make (Ordered);;

  let negateMember lit set = member (negate lit) set;;

  let negate =
        let f (lit,set) = add set (negate lit)
      in
        foldl f empty
      ;;

  let relations =
        let f (lit,set) = Name_arity.Set.add set (relation lit)
      in
        foldl f Name_arity.Set.empty
      ;;

  let functions =
        let f (lit,set) = Name_arity.Set.union set (functions lit)
      in
        foldl f Name_arity.Set.empty
      ;;

  let freeIn v = exists (freeIn v);;

  let freeVars =
        let f (lit,set) = Name.Set.union set (freeVars lit)
      in
        foldl f Name.Set.empty
      ;;

  let freeVarsList =
        let f (lits,set) = Name.Set.union set (freeVars lits)
      in
        Mlist.foldl f Name.Set.empty
      ;;

  let symbols =
        let f (lit,z) = symbols lit + z
      in
        foldl f 0
      ;;

  let typedSymbols =
        let f (lit,z) = typedSymbols lit + z
      in
        foldl f 0
      ;;

  let subst sub lits =
        let substLit (lit,(eq,lits')) =
              let lit' = subst sub lit
              in let eq = eq && Portable.pointerEqual (lit,lit')
            in
              (eq, add lits' lit')

        in let (eq,lits') = foldl substLit (true,empty) lits
      in
        if eq then lits else lits'
      ;;

  let conjoin set =
      Formula.listMkConj (List.map toFormula (toList set));;

  let disjoin set =
      Formula.listMkDisj (List.map toFormula (toList set));;

  let toString cl =
    "{" ^ String.concat ", " (List.map toString (toList cl)) ^ "}"

end

module Set_ordered =
struct type t = Set.set let compare = fromCompare Set.compare end

module Set_map = Mmap.Make (Set_ordered);;

module Set_set = Mset.Make (Set_ordered);;

end


(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS                         *)
(* ========================================================================= *)

module Thm = struct

open Useful;;
open Order

(* ------------------------------------------------------------------------- *)
(* An abstract type of first order logic theorems.                           *)
(* ------------------------------------------------------------------------- *)

type clause = Literal.Set.set;;

type inferenceType =
    Axiom
  | Assume
  | Subst
  | Factor
  | Resolve
  | Refl
  | Equality;;

type thm = Thm of clause * (inferenceType * thm list);;

type inference = inferenceType * thm list;;

(* ------------------------------------------------------------------------- *)
(* Theorem destructors.                                                      *)
(* ------------------------------------------------------------------------- *)

let clause (Thm (cl,_)) = cl;;

let inference (Thm (_,inf)) = inf;;

(* Tautologies *)

let isTautology th =
  let chk = function
      (_,None) -> None
    | ((pol,atm), Some set) ->
      if (pol && Atom.isRefl atm) || Atom.Set.member atm set then None
      else Some (Atom.Set.add set atm)
  in
      match Literal.Set.foldl chk (Some Atom.Set.empty) (clause th) with
        Some _ -> false
      | None -> true;;

(* Contradictions *)

let isContradiction th = Literal.Set.null (clause th);;

(* Unit theorems *)

let destUnit (Thm (cl,_)) =
    if Literal.Set.size cl = 1 then Literal.Set.pick cl
    else raise (Error "Thm.destUnit");;

let isUnit = can destUnit;;

(* Unit equality theorems *)

let destUnitEq th = Literal.destEq (destUnit th);;

let isUnitEq = can destUnitEq;;

(* Literals *)

let member lit (Thm (cl,_)) = Literal.Set.member lit cl;;

let negateMember lit (Thm (cl,_)) = Literal.Set.negateMember lit cl;;

(* ------------------------------------------------------------------------- *)
(* A total order.                                                            *)
(* ------------------------------------------------------------------------- *)

let compare (th1,th2) = Literal.Set.compare (clause th1, clause th2);;

let equal th1 th2 = Literal.Set.equal (clause th1) (clause th2);;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let freeIn v (Thm (cl,_)) = Literal.Set.freeIn v cl;;

let freeVars (Thm (cl,_)) = Literal.Set.freeVars cl;;


(* ------------------------------------------------------------------------- *)
(* Pretty-printing.                                                          *)
(* ------------------------------------------------------------------------- *)

open Format

let inferenceTypeToString = function
    Axiom -> "axiom"
  | Assume -> "assume"
  | Subst -> "subst"
  | Factor -> "factor"
  | Resolve -> "resolve"
  | Refl -> "refl"
  | Equality -> "equality"

let toString (Thm (cl, (infType, ths))) =
  inferenceTypeToString infType ^ ": " ^ Literal.Set.toString cl

let rec print_proof (Thm (cl, (infType, ths))) =
  print_string ("Inference: " ^ inferenceTypeToString infType);
  print_break 0 0;

  print_string ("Clauses: " ^ Literal.Set.toString cl);
  print_break 0 0;

  print_string "Theorems: ";
  if ths = []
  then print_string "<none>"
  else begin
    print_break 0 0;
    open_vbox 2;
    print_break 0 0;
    List.iter (print_proof) ths;
    close_box ()
  end;
  print_break 0 0


(* ------------------------------------------------------------------------- *)
(* Primitive rules of inference.                                             *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ----- axiom C                                                             *)
(*   C                                                                       *)
(* ------------------------------------------------------------------------- *)

let axiom cl = Thm (cl,(Axiom,[]));;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ----------- assume L                                                      *)
(*   L \/ ~L                                                                 *)
(* ------------------------------------------------------------------------- *)

let assume lit =
    Thm (Literal.Set.fromList [lit; Literal.negate lit], (Assume,[]));;

(* ------------------------------------------------------------------------- *)
(*    C                                                                      *)
(* -------- subst s                                                          *)
(*   C[s]                                                                    *)
(* ------------------------------------------------------------------------- *)

let subst sub (Thm (cl,inf) as th) =
      let cl' = Literal.Set.subst sub cl
    in
      if Portable.pointerEqual (cl,cl') then th
      else
        match inf with
          (Subst,_) -> Thm (cl',inf)
        | _ -> Thm (cl',(Subst,[th]))
    ;;

(* ------------------------------------------------------------------------- *)
(*   L \/ C    ~L \/ D                                                       *)
(* --------------------- resolve L                                           *)
(*        C \/ D                                                             *)
(*                                                                           *)
(* The literal L must occur in the first theorem, and the literal ~L must    *)
(* occur in the second theorem.                                              *)
(* ------------------------------------------------------------------------- *)

let resolve lit (Thm (cl1,_) as th1) (Thm (cl2,_) as th2) =
      let cl1' = Literal.Set.delete cl1 lit
      and cl2' = Literal.Set.delete cl2 (Literal.negate lit)
    in
      Thm (Literal.Set.union cl1' cl2', (Resolve,[th1;th2]))
    ;;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------- refl t                                                          *)
(*   t = t                                                                   *)
(* ------------------------------------------------------------------------- *)

let refl tm = Thm (Literal.Set.singleton (true, Atom.mkRefl tm), (Refl,[]));;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ------------------------ equality L p t                                   *)
(*   ~(s = t) \/ ~L \/ L'                                                    *)
(*                                                                           *)
(* where s is the subterm of L at path p, and L' is L with the subterm at    *)
(* path p being replaced by t.                                               *)
(* ------------------------------------------------------------------------- *)

let equality lit path t =
      let s = Literal.subterm lit path

      in let lit' = Literal.replace lit (path,t)

      in let eqLit = Literal.mkNeq (s,t)

      in let cl = Literal.Set.fromList [eqLit; Literal.negate lit; lit']
    in
      Thm (cl,(Equality,[]))
    ;;

end


(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC                                               *)
(* ========================================================================= *)

module Proof = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* A type of first order logic proofs.                                       *)
(* ------------------------------------------------------------------------- *)

type inference =
    Axiom of Literal.Set.set
  | Assume of Atom.atom
  | Subst of Substitute.subst * Thm.thm
  | Resolve of Atom.atom * Thm.thm * Thm.thm
  | Refl of Term.term
  | Equality of Literal.literal * Term.path * Term.term;;

type proof = (Thm.thm * inference) list;;


(* ------------------------------------------------------------------------- *)
(* Reconstructing single inferences.                                         *)
(* ------------------------------------------------------------------------- *)

let parents = function
    (Axiom _) -> []
  | (Assume _) -> []
  | (Subst (_,th)) -> [th]
  | (Resolve (_,th,th')) -> [th;th']
  | (Refl _) -> []
  | (Equality _) -> [];;

let inferenceToThm = function
    (Axiom cl) -> Thm.axiom cl
  | (Assume atm) -> Thm.assume (true,atm)
  | (Subst (sub,th)) -> Thm.subst sub th
  | (Resolve (atm,th,th')) -> Thm.resolve (true,atm) th th'
  | (Refl tm) -> Thm.refl tm
  | (Equality (lit,path,r)) -> Thm.equality lit path r;;

  let reconstructSubst cl cl' =
        let rec recon = function
            [] ->
(*MetisTrace3
              let () = Print.trace Literal.Set.pp "reconstructSubst: cl" cl
              let () = Print.trace Literal.Set.pp "reconstructSubst: cl'" cl'
*)
              raise (Bug "can't reconstruct Subst rule")
          | (([],sub) :: others) ->
            if Literal.Set.equal (Literal.Set.subst sub cl) cl' then sub
            else recon others
          | ((lit :: lits, sub) :: others) ->
              let checkLit (lit',acc) =
                  match total (Literal.matchLiterals sub lit) lit' with
                    None -> acc
                  | Some sub -> (lits,sub) :: acc
            in
              recon (Literal.Set.foldl checkLit others cl')
      in
        Substitute.normalize (recon [(Literal.Set.toList cl, Substitute.empty)])
      ;;

  let reconstructResolvant cl1 cl2 cl =
      (if not (Literal.Set.subset cl1 cl) then
         Literal.Set.pick (Literal.Set.difference cl1 cl)
       else if not (Literal.Set.subset cl2 cl) then
         Literal.negate (Literal.Set.pick (Literal.Set.difference cl2 cl))
       else
         (* A useless resolution, but we must reconstruct it anyway *)
           let cl1' = Literal.Set.negate cl1
           and cl2' = Literal.Set.negate cl2
           in let lits = Literal.Set.intersectList [cl1;cl1';cl2;cl2']
         in
           if not (Literal.Set.null lits) then Literal.Set.pick lits
           else raise (Bug "can't reconstruct Resolve rule")
         );;

  let reconstructEquality cl =
(*MetisTrace3
        let () = Print.trace Literal.Set.pp "Proof.reconstructEquality: cl" cl
*)

        let rec sync s t path (f,a) (f',a') =
            if not (Name.equal f f' && length a = length a') then None
            else
                let itms = enumerate (zip a a')
              in
                (match List.filter (fun x -> not (uncurry Term.equal (snd x))) itms with
                  [(i,(tm,tm'))] ->
                    let path = i :: path
                  in
                    if Term.equal tm s && Term.equal tm' t then
                      Some (List.rev path)
                    else
                      (match (tm,tm') with
                        (Term.Fn f_a, Term.Fn f_a') -> sync s t path f_a f_a'
                      | _ -> None)
                | _ -> None)

        in let recon (neq,(pol,atm),(pol',atm')) =
            if pol = pol' then None
            else
                let (s,t) = Literal.destNeq neq

                in let path =
                    if not (Term.equal s t) then sync s t [] atm atm'
                    else if not (Atom.equal atm atm') then None
                    else Atom.find (Term.equal s) atm
              in
                match path with
                  Some path -> Some ((pol',atm),path,t)
                | None -> None

        in let candidates =
            match List.partition Literal.isNeq (Literal.Set.toList cl) with
              ([l1],[l2;l3]) -> [(l1,l2,l3);(l1,l3,l2)]
            | ([l1;l2],[l3]) -> [(l1,l2,l3);(l1,l3,l2);(l2,l1,l3);(l2,l3,l1)]
            | ([l1],[l2]) -> [(l1,l1,l2);(l1,l2,l1)]
            | _ -> raise (Bug "reconstructEquality: malformed")

(*MetisTrace3
        let ppCands =
            Print.ppList (Print.ppTriple Literal.pp Literal.pp Literal.pp)
        let () = Print.trace ppCands
                   "Proof.reconstructEquality: candidates" candidates
*)
      in
        match first recon candidates with
          Some info -> info
        | None -> raise (Bug "can't reconstruct Equality rule")
      ;;

  let reconstruct cl = function
      (Thm.Axiom,[]) -> Axiom cl
    | (Thm.Assume,[]) ->
      (match Literal.Set.findl Literal.positive cl with
         Some (_,atm) -> Assume atm
       | None -> raise (Bug "malformed Assume inference"))
    | (Thm.Subst,[th]) ->
      Subst (reconstructSubst (Thm.clause th) cl, th)
    | (Thm.Resolve,[th1;th2]) ->
        let cl1 = Thm.clause th1
        and cl2 = Thm.clause th2
        in let (pol,atm) = reconstructResolvant cl1 cl2 cl
      in
        if pol then Resolve (atm,th1,th2) else Resolve (atm,th2,th1)
    | (Thm.Refl,[]) ->
      (match Literal.Set.findl (kComb true) cl with
         Some lit -> Refl (Literal.destRefl lit)
       | None -> raise (Bug "malformed Refl inference"))
    | (Thm.Equality,[]) -> let (x,y,z) = (reconstructEquality cl) in Equality (x,y,z)
    | _ -> raise (Bug "malformed inference");;

  let thmToInference th =
(*MetisTrace3
        let () = Print.trace Thm.pp "Proof.thmToInference: th" th
*)

        let cl = Thm.clause th

        in let thmInf = Thm.inference th

(*MetisTrace3
        let ppThmInf = Print.ppPair Thm.ppInferenceType (Print.ppList Thm.pp)
        let () = Print.trace ppThmInf "Proof.thmToInference: thmInf" thmInf
*)

        in let inf = reconstruct cl thmInf

(*MetisTrace3
        let () = Print.trace ppInference "Proof.thmToInference: inf" inf
*)
      in
        inf
;;

(* ------------------------------------------------------------------------- *)
(* Reconstructing whole proofs.                                              *)
(* ------------------------------------------------------------------------- *)

let proof th =
  let emptyThms : Thm.thm Literal.Set_map.map = Literal.Set_map.newMap ()

  in let rec addThms (th,ths) =
        let cl = Thm.clause th
      in
        if Literal.Set_map.inDomain cl ths then ths
        else
            let (_,pars) = Thm.inference th
            in let ths = Mlist.foldl addThms ths pars
          in
            if Literal.Set_map.inDomain cl ths then ths
            else Literal.Set_map.insert ths (cl,th)

  in let mkThms th = addThms (th,emptyThms)

  in let rec addProof (th,(ths,acc)) =
        let cl = Thm.clause th
      in
        match Literal.Set_map.peek ths cl with
          None -> (ths,acc)
        | Some th ->
            let (_,pars) = Thm.inference th
            in let (ths,acc) = Mlist.foldl addProof (ths,acc) pars
            in let ths = Literal.Set_map.delete ths cl
            in let acc = (th, thmToInference th) :: acc
          in
            (ths,acc)

  in let mkProof ths th =
        let (ths,acc) = addProof (th,(ths,[]))
(*MetisTrace4
        let () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (Literal.Set_map.size ths)
*)
      in
        List.rev acc

(*MetisTrace3
        let () = Print.trace Thm.pp "Proof.proof: th" th
*)
  in    let ths = mkThms th
        in let infs = mkProof ths th
(*MetisTrace3
        let () = Print.trace Print.ppInt "Proof.proof: size" (length infs)
*)
      in
        infs
      ;;

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

let freeIn v =
      let free th_inf =
          match th_inf with
            (_, Axiom lits) -> Literal.Set.freeIn v lits
          | (_, Assume atm) -> Atom.freeIn v atm
          | (th, Subst _) -> Thm.freeIn v th
          | (_, Resolve _) -> false
          | (_, Refl tm) -> Term.freeIn v tm
          | (_, Equality (lit,_,tm)) ->
            Literal.freeIn v lit || Term.freeIn v tm
    in
      List.exists free
    ;;

let freeVars =
      let inc (th_inf,set) =
          Name.Set.union set
          (match th_inf with
             (_, Axiom lits) -> Literal.Set.freeVars lits
           | (_, Assume atm) -> Atom.freeVars atm
           | (th, Subst _) -> Thm.freeVars th
           | (_, Resolve _) -> Name.Set.empty
           | (_, Refl tm) -> Term.freeVars tm
           | (_, Equality (lit,_,tm)) ->
             Name.Set.union (Literal.freeVars lit) (Term.freeVars tm))
    in
      Mlist.foldl inc Name.Set.empty
    ;;

end


(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
(* ========================================================================= *)

module Rule = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* Variable names.                                                           *)
(* ------------------------------------------------------------------------- *)

let xVarName = Name.fromString "x";;
let xVar = Term.Var xVarName;;

let yVarName = Name.fromString "y";;
let yVar = Term.Var yVarName;;

let zVarName = Name.fromString "z";;
let zVar = Term.Var zVarName;;

let xIVarName i = Name.fromString ("x" ^ Int.toString i);;
let xIVar i = Term.Var (xIVarName i);;

let yIVarName i = Name.fromString ("y" ^ Int.toString i);;
let yIVar i = Term.Var (yIVarName i);;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------- reflexivity                                                     *)
(*   x = x                                                                   *)
(* ------------------------------------------------------------------------- *)

let reflexivityRule x = Thm.refl x;;

let reflexivity = reflexivityRule xVar;;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------------------- symmetry                                            *)
(*   ~(x = y) \/ y = x                                                       *)
(* ------------------------------------------------------------------------- *)

let symmetryRule x y =
      let reflTh = reflexivityRule x
      in let reflLit = Thm.destUnit reflTh
      in let eqTh = Thm.equality reflLit [0] y
    in
      Thm.resolve reflLit reflTh eqTh
    ;;

let symmetry = symmetryRule xVar yVar;;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* --------------------------------- transitivity                            *)
(*   ~(x = y) \/ ~(y = z) \/ x = z                                           *)
(* ------------------------------------------------------------------------- *)

let transitivity =
      let eqTh = Thm.equality (Literal.mkEq (yVar,zVar)) [0] xVar
    in
      Thm.resolve (Literal.mkEq (yVar,xVar)) symmetry eqTh
    ;;

(* ------------------------------------------------------------------------- *)
(*   x = y \/ C                                                              *)
(* -------------- symEq (x = y)                                              *)
(*   y = x \/ C                                                              *)
(* ------------------------------------------------------------------------- *)

let symEq lit th =
      let (x,y) = Literal.destEq lit
    in
      if Term.equal x y then th
      else
          let sub = Substitute.fromList [(xVarName,x);(yVarName,y)]

          in let symTh = Thm.subst sub symmetry
        in
          Thm.resolve lit th symTh
    ;;

(* ------------------------------------------------------------------------- *)
(* An equation consists of two terms (t,u) plus a theorem (stronger than)    *)
(* t = u \/ C.                                                               *)
(* ------------------------------------------------------------------------- *)

type equation = (Term.term * Term.term) * Thm.thm;;

let equationLiteral (t_u,th) =
      let lit = Literal.mkEq t_u
    in
      if Literal.Set.member lit (Thm.clause th) then Some lit else None
    ;;

let reflEqn t = ((t,t), Thm.refl t);;

let symEqn (((t,u), th) as eqn) =
    if Term.equal t u then eqn
    else
      ((u,t),
       match equationLiteral eqn with
         Some t_u -> symEq t_u th
       | None -> th);;

let transEqn (((x,y), th1) as eqn1) (((_,z), th2) as eqn2) =
    if Term.equal x y then eqn2
    else if Term.equal y z then eqn1
    else if Term.equal x z then reflEqn x
    else
      ((x,z),
       match equationLiteral eqn1 with
         None -> th1
       | Some x_y ->
         match equationLiteral eqn2 with
           None -> th2
         | Some y_z ->
             let sub = Substitute.fromList [(xVarName,x);(yVarName,y);(zVarName,z)]
             in let th = Thm.subst sub transitivity
             in let th = Thm.resolve x_y th1 th
             in let th = Thm.resolve y_z th2 th
           in
             th
           );;

(* ------------------------------------------------------------------------- *)
(* A conversion takes a term t and either:                                   *)
(* 1. Returns a term u together with a theorem (stronger than) t = u \/ C.   *)
(* 2. Raises an Error exception.                                             *)
(* ------------------------------------------------------------------------- *)

type conv = Term.term -> Term.term * Thm.thm;;

let allConv tm = (tm, Thm.refl tm);;

let noConv : conv = fun _ -> raise (Error "noConv");;


let thenConvTrans tm (tm',th1) (tm'',th2) =
      let eqn1 = ((tm,tm'),th1)
      and eqn2 = ((tm',tm''),th2)
      in let (_,th) = transEqn eqn1 eqn2
    in
      (tm'',th)
    ;;

let thenConv conv1 conv2 tm =
      let (tm',_) as res1 = conv1 tm
      in let res2 = conv2 tm'
    in
      thenConvTrans tm res1 res2
    ;;

let orelseConv (conv1 : conv) conv2 tm = try conv1 tm with Error _ -> conv2 tm;;

let tryConv conv = orelseConv conv allConv;;

let changedConv conv tm =
      let (tm',_) as res = conv tm
    in
      if tm = tm' then raise (Error "changedConv") else res
    ;;

let rec repeatConv conv tm = tryConv (thenConv conv (repeatConv conv)) tm;;

let flip f = fun x y -> f y x;;

let rec firstConv tm = function
    [] -> raise (Error "firstConv")
  | [conv] -> conv tm
  | (conv :: convs) -> orelseConv conv (flip firstConv convs) tm;;
let firstConv convs tm = firstConv tm convs;;

let rec everyConv tm = function
    [] -> allConv tm
  | [conv] -> conv tm
  | (conv :: convs) -> thenConv conv (flip everyConv convs) tm;;
let everyConv convs tm = everyConv tm convs;;

let rewrConv (((x,y), eqTh) as eqn) path tm =
    if Term.equal x y then allConv tm
    else if Mlist.null path then (y,eqTh)
    else
        let reflTh = Thm.refl tm
        in let reflLit = Thm.destUnit reflTh
        in let th = Thm.equality reflLit (1 :: path) y
        in let th = Thm.resolve reflLit reflTh th
        in let th =
            match equationLiteral eqn with
              None -> th
            | Some x_y -> Thm.resolve x_y eqTh th
        in let tm' = Term.replace tm (path,y)
      in
        (tm',th)
      ;;

let pathConv conv path tm =
      let x = Term.subterm tm path
      in let (y,th) = conv x
    in
      rewrConv ((x,y),th) path tm
    ;;

let subtermConv conv i = pathConv conv [i];;

let subtermsConv conv = function
    (Term.Var _ as tm) -> allConv tm
  | (Term.Fn (_,a) as tm) ->
    everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;;

(* ------------------------------------------------------------------------- *)
(* Applying a conversion to every subterm, with some traversal strategy.     *)
(* ------------------------------------------------------------------------- *)

let rec bottomUpConv conv tm =
    thenConv (subtermsConv (bottomUpConv conv)) (repeatConv conv) tm;;

let rec topDownConv conv tm =
    thenConv (repeatConv conv) (subtermsConv (topDownConv conv)) tm;;

let repeatTopDownConv conv =
      let rec f tm = thenConv (repeatConv conv) g tm
      and g tm = thenConv (subtermsConv f) h tm
      and h tm = tryConv (thenConv conv f) tm
    in
      f
    ;;

(* ------------------------------------------------------------------------- *)
(* A literule (bad pun) takes a literal L and either:                        *)
(* 1. Returns a literal L' with a theorem (stronger than) ~L \/ L' \/ C.     *)
(* 2. Raises an Error exception.                                             *)
(* ------------------------------------------------------------------------- *)

type literule = Literal.literal -> Literal.literal * Thm.thm;;

let allLiterule lit = (lit, Thm.assume lit);;

let noLiterule : literule = fun _ -> raise (Error "noLiterule");;

let thenLiterule literule1 literule2 lit =
      let (lit',th1) as res1 = literule1 lit
      in let (lit'',th2) as res2 = literule2 lit'
    in
      if Literal.equal lit lit' then res2
      else if Literal.equal lit' lit'' then res1
      else if Literal.equal lit lit'' then allLiterule lit
      else
        (lit'',
         if not (Thm.member lit' th1) then th1
         else if not (Thm.negateMember lit' th2) then th2
         else Thm.resolve lit' th1 th2)
    ;;

let orelseLiterule (literule1 : literule) literule2 lit =
    try literule1 lit with Error _ -> literule2 lit;;

let tryLiterule literule = orelseLiterule literule allLiterule;;

let changedLiterule literule lit =
      let (lit',_) as res = literule lit
    in
      if lit = lit' then raise (Error "changedLiterule") else res
    ;;

let rec repeatLiterule literule lit =
    tryLiterule (thenLiterule literule (repeatLiterule literule)) lit;;

let rec firstLiterule lit = function
    [] -> raise (Error "firstLiterule")
  | [literule] -> literule lit
  | (literule :: literules) ->
    orelseLiterule literule (flip firstLiterule literules) lit;;
let firstLiterule literules lit = firstLiterule lit literules;;

let rec everyLiterule lit = function
    [] -> allLiterule lit
  | [literule] -> literule lit
  | (literule :: literules) ->
    thenLiterule literule (flip everyLiterule literules) lit;;
let everyLiterule literules lit = everyLiterule lit literules;;

let rewrLiterule (((x,y),eqTh) as eqn) path lit =
    if Term.equal x y then allLiterule lit
    else
        let th = Thm.equality lit path y
        in let th =
            match equationLiteral eqn with
              None -> th
            | Some x_y -> Thm.resolve x_y eqTh th
        in let lit' = Literal.replace lit (path,y)
      in
        (lit',th)
      ;;

let pathLiterule conv path lit =
      let tm = Literal.subterm lit path
      in let (tm',th) = conv tm
    in
      rewrLiterule ((tm,tm'),th) path lit
    ;;

let argumentLiterule conv i = pathLiterule conv [i];;

let allArgumentsLiterule conv lit =
    everyLiterule
      (List.map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;;

(* ------------------------------------------------------------------------- *)
(* A rule takes one theorem and either deduces another or raises an Error    *)
(* exception.                                                                *)
(* ------------------------------------------------------------------------- *)

type rule = Thm.thm -> Thm.thm;;

let allRule : rule = fun th -> th;;

let noRule : rule = fun _ -> raise (Error "noRule");;

let thenRule (rule1 : rule) (rule2 : rule) th = rule1 (rule2 th);;

let orelseRule (rule1 : rule) rule2 th = try rule1 th with Error _ -> rule2 th;;

let tryRule rule = orelseRule rule allRule;;

let changedRule rule th =
      let th' = rule th
    in
      if not (Literal.Set.equal (Thm.clause th) (Thm.clause th')) then th'
      else raise (Error "changedRule")
    ;;

let rec repeatRule rule lit = tryRule (thenRule rule (repeatRule rule)) lit;;

let rec firstRule th = function
    [] -> raise (Error "firstRule")
  | [rule] -> rule th
  | (rule :: rules) -> orelseRule rule (flip firstRule rules) th;;
let firstRule rules th = firstRule th rules;;

let rec everyRule th = function
    [] -> allRule th
  | [rule] -> rule th
  | (rule :: rules) -> thenRule rule (flip everyRule rules) th;;
let everyRule rules th = everyRule th rules;;

let literalRule literule lit th =
      let (lit',litTh) = literule lit
    in
      if Literal.equal lit lit' then th
      else if not (Thm.negateMember lit litTh) then litTh
      else Thm.resolve lit th litTh
    ;;

let rewrRule eqTh lit path = literalRule (rewrLiterule eqTh path) lit;;

let pathRule conv lit path = literalRule (pathLiterule conv path) lit;;

let literalsRule literule =
      let f (lit,th) =
          if Thm.member lit th then literalRule literule lit th else th
    in
      fun lits -> fun th -> Literal.Set.foldl f th lits
    ;;

let allLiteralsRule literule th = literalsRule literule (Thm.clause th) th;;

let convRule conv = allLiteralsRule (allArgumentsLiterule conv);;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ---------------------------------------------- functionCongruence (f,n)   *)
(*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
(*   f x0 ... x{n-1} = f y0 ... y{n-1}                                       *)
(* ------------------------------------------------------------------------- *)

let functionCongruence (f,n) =
      let xs = Mlist.tabulate (n,xIVar)
      and ys = Mlist.tabulate (n,yIVar)

      in let cong ((i,yi),(th,lit)) =
            let path = [1;i]
            in let th = Thm.resolve lit th (Thm.equality lit path yi)
            in let lit = Literal.replace lit (path,yi)
          in
            (th,lit)

      in let reflTh = Thm.refl (Term.Fn (f,xs))
      in let reflLit = Thm.destUnit reflTh
    in
      fst (Mlist.foldl cong (reflTh,reflLit) (enumerate ys))
    ;;

(* ------------------------------------------------------------------------- *)
(*                                                                           *)
(* ---------------------------------------------- relationCongruence (R,n)   *)
(*   ~(x0 = y0) \/ ... \/ ~(x{n-1} = y{n-1}) \/                              *)
(*   ~R x0 ... x{n-1} \/ R y0 ... y{n-1}                                     *)
(* ------------------------------------------------------------------------- *)

let relationCongruence (r,n) =
      let xs = Mlist.tabulate (n,xIVar)
      and ys = Mlist.tabulate (n,yIVar)

      in let cong ((i,yi),(th,lit)) =
            let path = [i]
            in let th = Thm.resolve lit th (Thm.equality lit path yi)
            in let lit = Literal.replace lit (path,yi)
          in
            (th,lit)

      in let assumeLit = (false,(r,xs))
      in let assumeTh = Thm.assume assumeLit
    in
      fst (Mlist.foldl cong (assumeTh,assumeLit) (enumerate ys))
    ;;

(* ------------------------------------------------------------------------- *)
(*   ~(x = y) \/ C                                                           *)
(* ----------------- symNeq ~(x = y)                                         *)
(*   ~(y = x) \/ C                                                           *)
(* ------------------------------------------------------------------------- *)

let symNeq lit th =
      let (x,y) = Literal.destNeq lit
    in
      if Term.equal x y then th
      else
          let sub = Substitute.fromList [(xVarName,y);(yVarName,x)]
          in let symTh = Thm.subst sub symmetry
        in
          Thm.resolve lit th symTh
    ;;

(* ------------------------------------------------------------------------- *)
(* sym (x = y) = symEq (x = y)  /\  sym ~(x = y) = symNeq ~(x = y)           *)
(* ------------------------------------------------------------------------- *)

let sym ((pol,_) as lit) th = if pol then symEq lit th else symNeq lit th;;

(* ------------------------------------------------------------------------- *)
(*   ~(x = x) \/ C                                                           *)
(* ----------------- removeIrrefl                                            *)
(*         C                                                                 *)
(*                                                                           *)
(* where all irreflexive equalities.                                         *)
(* ------------------------------------------------------------------------- *)

let removeIrrefl th =
  let irrefl = function
      ((true,_),th) -> th
    | ((false,atm) as lit, th) ->
      match total Atom.destRefl atm with
        Some x -> Thm.resolve lit th (Thm.refl x)
      | None -> th
in
  Literal.Set.foldl irrefl th (Thm.clause th);;

(* ------------------------------------------------------------------------- *)
(*   x = y \/ y = x \/ C                                                     *)
(* ----------------------- removeSym                                         *)
(*       x = y \/ C                                                          *)
(*                                                                           *)
(* where all duplicate copies of equalities and disequalities are removed.   *)
(* ------------------------------------------------------------------------- *)

let removeSym th =
  let rem ((pol,atm) as lit, (eqs,th)) =
      match total Atom.sym atm with
        None -> (eqs, th)
      | Some atm' ->
        if Literal.Set.member lit eqs then
          (eqs, if pol then symEq lit th else symNeq lit th)
        else
          (Literal.Set.add eqs (pol,atm'), th)
in
      snd (Literal.Set.foldl rem (Literal.Set.empty,th) (Thm.clause th));;

(* ------------------------------------------------------------------------- *)
(*   ~(v = t) \/ C                                                           *)
(* ----------------- expandAbbrevs                                           *)
(*      C[t/v]                                                               *)
(*                                                                           *)
(* where t must not contain any occurrence of the variable v.                *)
(* ------------------------------------------------------------------------- *)

let rec expandAbbrevs th =
  let expand lit =
        let (x,y) = Literal.destNeq lit
        in let _ = Term.isTypedVar x || Term.isTypedVar y ||
                raise (Error "Rule.expandAbbrevs: no vars")
        in let _ = not (Term.equal x y) ||
                raise (Error "Rule.expandAbbrevs: equal vars")
      in
        Substitute.unify Substitute.empty x y
in
      match Literal.Set.firstl (total expand) (Thm.clause th) with
        None -> removeIrrefl th
      | Some sub -> expandAbbrevs (Thm.subst sub th);;

(* ------------------------------------------------------------------------- *)
(* simplify = isTautology + expandAbbrevs + removeSym                        *)
(* ------------------------------------------------------------------------- *)

let rec simplify th =
    if Thm.isTautology th then None
    else
        let th' = th
        in let th' = expandAbbrevs th'
        in let th' = removeSym th'
      in
        if Thm.equal th th' then Some th else simplify th'
      ;;

(* ------------------------------------------------------------------------- *)
(*    C                                                                      *)
(* -------- freshVars                                                        *)
(*   C[s]                                                                    *)
(*                                                                           *)
(* where s is a renaming substitution chosen so that all of the variables in *)
(* C are replaced by fresh variables.                                        *)
(* ------------------------------------------------------------------------- *)

let freshVars th = Thm.subst (Substitute.freshVars (Thm.freeVars th)) th;;

(* ------------------------------------------------------------------------- *)
(*               C                                                           *)
(* ---------------------------- factor                                       *)
(*   C_s_1, C_s_2, ..., C_s_n                                                *)
(*                                                                           *)
(* where each s_i is a substitution that factors C, meaning that the theorem *)
(*                                                                           *)
(*   C_s_i = (removeIrrefl o removeSym o Thm.subst s_i) C                    *)
(*                                                                           *)
(* has fewer literals than C.                                                *)
(*                                                                           *)
(* Also, if s is any substitution that factors C, then one of the s_i will   *)
(* result in a theorem C_s_i that strictly subsumes the theorem C_s.         *)
(* ------------------------------------------------------------------------- *)

  type edge =
      Factor_edge of Atom.atom * Atom.atom
    | Refl_edge of Term.term * Term.term;;

  type joinStatus =
      Joined
    | Joinable of Substitute.subst
    | Apart;;

  let joinEdge sub edge =
        let result =
            match edge with
              Factor_edge (atm,atm') -> total (Atom.unify sub atm) atm'
            | Refl_edge (tm,tm') -> total (Substitute.unify sub tm) tm'
      in
        match result with
          None -> Apart
        | Some sub' ->
          if Portable.pointerEqual (sub,sub') then Joined else Joinable sub'
      ;;

  let updateApart sub =
        let rec update acc = function
            [] -> Some acc
          | (edge :: edges) ->
            match joinEdge sub edge with
              Joined -> None
            | Joinable _ -> update (edge :: acc) edges
            | Apart -> update acc edges
      in
        update []
      ;;

  let addFactorEdge (pol,atm) ((pol',atm'),acc) =
      if pol <> pol' then acc
      else
          let edge = Factor_edge (atm,atm')
        in
          match joinEdge Substitute.empty edge with
            Joined -> raise (Bug "addFactorEdge: joined")
          | Joinable sub -> (sub,edge) :: acc
          | Apart -> acc
        ;;

  let addReflEdge = function
      ((false,_), acc) -> acc
    | ((true,atm), acc) ->
        let edge = let (x,y) = (Atom.destEq atm) in Refl_edge (x,y)
      in
        match joinEdge Substitute.empty edge with
          Joined -> raise (Bug "addRefl: joined")
        | Joinable _ -> edge :: acc
        | Apart -> acc
      ;;
  let addReflEdge = curry addReflEdge;;

  let addIrreflEdge = function
      ((true,_), acc) -> acc
    | ((false,atm), acc) ->
        let edge = let (x,y) = (Atom.destEq atm) in Refl_edge (x,y)
      in
        match joinEdge Substitute.empty edge with
          Joined -> raise (Bug "addRefl: joined")
        | Joinable sub -> (sub,edge) :: acc
        | Apart -> acc
      ;;
  let addIrreflEdge = curry addIrreflEdge;;

  let rec init_edges acc apart = function
      [] ->
        let init ((apart,sub,edge),(edges,acc)) =
            (edge :: edges, (apart,sub,edges) :: acc)
      in
        snd (Mlist.foldl init ([],[]) acc)
    | ((sub,edge) :: sub_edges) ->
        let (acc,apart) =
            match updateApart sub apart with
              Some apart' -> ((apart',sub,edge) :: acc, edge :: apart)
            | None -> (acc,apart)
      in
        init_edges acc apart sub_edges
      ;;

  let rec mk_edges apart sub_edges = function
      [] -> init_edges [] apart sub_edges
    | (lit :: lits) ->
        let sub_edges = Mlist.foldl (addFactorEdge lit) sub_edges lits

        in let (apart,sub_edges) =
            match total Literal.sym lit with
              None -> (apart,sub_edges)
            | Some lit' ->
                let apart = addReflEdge lit apart
                in let sub_edges = addIrreflEdge lit sub_edges
                in let sub_edges = Mlist.foldl (addFactorEdge lit') sub_edges lits
              in
                (apart,sub_edges)
      in
        mk_edges apart sub_edges lits
      ;;

  let rec fact acc = function
      [] -> acc
    | ((_,sub,[]) :: others) -> fact (sub :: acc) others
    | ((apart, sub, edge :: edges) :: others) ->
        let others =
            match joinEdge sub edge with
              Joinable sub' ->
                let others = (edge :: apart, sub, edges) :: others
              in
                (match updateApart sub' apart with
                  None -> others
                | Some apart' -> (apart',sub',edges) :: others)
            | _ -> (apart,sub,edges) :: others
      in
        fact acc others
      ;;

  let factor' cl =
(*MetisTrace6
        let () = Print.trace Literal.Set.pp "Rule.factor': cl" cl
*)
        let edges = mk_edges [] [] (Literal.Set.toList cl)
(*MetisTrace6
        let ppEdgesSize = Print.ppMap length Print.ppInt
        let ppEdgel = Print.ppList ppEdge
        let ppEdges = Print.ppList (Print.ppTriple ppEdgel Substitute.pp ppEdgel)
        let () = Print.trace ppEdgesSize "Rule.factor': |edges|" edges
        let () = Print.trace ppEdges "Rule.factor': edges" edges
*)
        in let result = fact [] edges
(*MetisTrace6
        let ppResult = Print.ppList Substitute.pp
        let () = Print.trace ppResult "Rule.factor': result" result
*)
      in
        result
      ;;

let factor th =
      let fact sub = removeIrrefl (removeSym (Thm.subst sub th))
    in
      List.map fact (factor' (Thm.clause th))
    ;;


end

(* ========================================================================= *)
(* RANDOM FINITE MODELS                                                      *)
(* ========================================================================= *)

module Model = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* Constants.                                                                *)
(* ------------------------------------------------------------------------- *)

let maxSpace = 1000;;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

let multInt =
    match Int.maxInt with
      None -> (fun x -> fun y -> Some (x * y))
    | Some m ->
        let m = Real.floor (Math.sqrt (Real.fromInt m))
      in
        fun x -> fun y -> if x <= m && y <= m then Some (x * y) else None
      ;;

  let rec iexp x y acc =
      if y mod 2 = 0 then iexp' x y acc
      else
        match multInt acc x with
          Some acc -> iexp' x y acc
        | None -> None

  and iexp' x y acc =
      if y = 1 then Some acc
      else
          let y = Int.div y 2
        in
          match multInt x x with
            Some x -> iexp x y acc
          | None -> None
        ;;

  let expInt x y =
      if y <= 1 then
        if y = 0 then Some 1
        else if y = 1 then Some x
        else raise (Bug "expInt: negative exponent")
      else if x <= 1 then
        if 0 <= x then Some x
        else raise (Bug "expInt: negative exponand")
      else iexp x y 1;;

let boolToInt = function
    true -> 1
  | false -> 0;;

let intToBool = function
    1 -> true
  | 0 -> false
  | _ -> raise (Bug "Model.intToBool");;

let minMaxInterval i j = interval i (1 + j - i);;

(* ------------------------------------------------------------------------- *)
(* Model size.                                                               *)
(* ------------------------------------------------------------------------- *)

type size = {size : int};;

(* ------------------------------------------------------------------------- *)
(* A model of size N has integer elements 0...N-1.                           *)
(* ------------------------------------------------------------------------- *)

type element = int;;

let zeroElement = 0;;

let incrementElement s i =
    let n = s.size in
    let i = i + 1 in
      if i = n then None else Some i
    ;;

let elementListSpace s arity =
  let n = s.size in
    match expInt n arity with
      None -> None
    | Some m as s -> if m <= maxSpace then s else None;;

let elementListIndex s =
    let n = s.size in
      let rec f acc elts =
          match elts with
            [] -> acc
          | elt :: elts -> f (n * acc + elt) elts
    in
      f 0
    ;;

(* ------------------------------------------------------------------------- *)
(* The parts of the model that are fixed.                                    *)
(* ------------------------------------------------------------------------- *)

type fixedFunction = size -> element list -> element option;;

type fixedRelation = size -> element list -> bool option;;

type fixed =
      {functions : fixedFunction Name_arity.Map.map;
       relations : fixedRelation Name_arity.Map.map};;

let uselessFixedFunction : fixedFunction = kComb (kComb None);;

let uselessFixedRelation : fixedRelation = kComb (kComb None);;

let emptyFunctions : fixedFunction Name_arity.Map.map = Name_arity.Map.newMap ();;

let emptyRelations : fixedRelation Name_arity.Map.map = Name_arity.Map.newMap ();;

let fixed0 f sz elts =
    match elts with
      [] -> f sz
    | _ -> raise (Bug "Model.fixed0: wrong arity");;

let fixed1 f sz elts =
    match elts with
      [x] -> f sz x
    | _ -> raise (Bug "Model.fixed1: wrong arity");;

let fixed2 f sz elts =
    match elts with
      [x;y] -> f sz x y
    | _ -> raise (Bug "Model.fixed2: wrong arity");;

let emptyFixed =
      let fns = emptyFunctions
      and rels = emptyRelations
    in
        {functions = fns;
         relations = rels}
    ;;

let peekFunctionFixed fix name_arity =
      Name_arity.Map.peek fix.functions name_arity
    ;;

let peekRelationFixed fix name_arity =
      Name_arity.Map.peek fix.relations name_arity
    ;;

let getFunctionFixed fix name_arity =
    match peekFunctionFixed fix name_arity with
      Some f -> f
    | None -> uselessFixedFunction;;

let getRelationFixed fix name_arity =
    match peekRelationFixed fix name_arity with
      Some rel -> rel
    | None -> uselessFixedRelation;;

let insertFunctionFixed fix name_arity_fun =
    let fns = Name_arity.Map.insert fix.functions name_arity_fun
    in
        {functions = fns;
         relations = fix.relations}
    ;;

let insertRelationFixed fix name_arity_rel =
    let rels = Name_arity.Map.insert fix.relations name_arity_rel
    in
        {functions = fix.functions;
         relations = rels}
    ;;

  let union _ = raise (Bug "Model.unionFixed: nameArity clash");;
  let unionFixed fix1 fix2 =
        let fns = Name_arity.Map.union union fix1.functions fix2.functions in
        let rels = Name_arity.Map.union union fix1.relations fix2.relations in
          {functions = fns;
           relations = rels}
      ;;

let unionListFixed =
      let union (fix,acc) = unionFixed acc fix
    in
      Mlist.foldl union emptyFixed
    ;;

  let hasTypeFn _ elts =
      match elts with
        [x;_] -> Some x
      | _ -> raise (Bug "Model.hasTypeFn: wrong arity");;

  let eqRel _ elts =
      match elts with
        [x;y] -> Some (x = y)
      | _ -> raise (Bug "Model.eqRel: wrong arity");;

  let basicFixed =
        let fns = Name_arity.Map.singleton (Term.hasTypeFunction,hasTypeFn)

        in let rels = Name_arity.Map.singleton (Atom.eqRelation,eqRel)
      in
          {functions = fns;
           relations = rels}
      ;;

(* ------------------------------------------------------------------------- *)
(* Renaming fixed model parts.                                               *)
(* ------------------------------------------------------------------------- *)

type fixedMap =
     {functionMap : Name.name Name_arity.Map.map;
      relationMap : Name.name Name_arity.Map.map};;

let mapFixed fixMap fix =
      let fnMap = fixMap.functionMap in
      let relMap = fixMap.relationMap in
      let fns = fix.functions in
      let rels = fix.relations in
      let fns = Name_arity.Map.compose fnMap fns in
      let rels = Name_arity.Map.compose relMap rels in
        {functions = fns;
         relations = rels}
    ;;


(* ------------------------------------------------------------------------- *)
(* Standard fixed model parts.                                               *)
(* ------------------------------------------------------------------------- *)

(* Projections *)

let projectionMin = 1
and projectionMax = 9;;

let projectionList = minMaxInterval projectionMin projectionMax;;

let projectionName i =
      let _ = projectionMin <= i ||
              raise (Bug "Model.projectionName: less than projectionMin")

      in let _ = i <= projectionMax ||
              raise (Bug "Model.projectionName: greater than projectionMax")
    in
      Name.fromString ("project" ^ Int.toString i)
    ;;

let projectionFn i _ elts = Some (Mlist.nth (elts, i - 1));;

let arityProjectionFixed arity =
      let mkProj i = ((projectionName i, arity), projectionFn i)

      in let rec addProj i acc =
          if i > arity then acc
          else addProj (i + 1) (Name_arity.Map.insert acc (mkProj i))

      in let fns = addProj projectionMin emptyFunctions

      in let rels = emptyRelations
    in
        {functions = fns;
         relations = rels}
    ;;

let projectionFixed =
    unionListFixed (List.map arityProjectionFixed projectionList);;

(* Arithmetic *)

let numeralMin = -100
and numeralMax = 100;;

let numeralList = minMaxInterval numeralMin numeralMax;;

let numeralName i =
      let _ = numeralMin <= i ||
              raise (Bug "Model.numeralName: less than numeralMin")

      in let _ = i <= numeralMax ||
              raise (Bug "Model.numeralName: greater than numeralMax")

      in let s = if i < 0 then "negative" ^ Int.toString (-i) else Int.toString i
    in
      Name.fromString s
    ;;

let addName = Name.fromString "+"
and divName = Name.fromString "div"
and dividesName = Name.fromString "divides"
and evenName = Name.fromString "even"
and expName = Name.fromString "exp"
and geName = Name.fromString ">="
and gtName = Name.fromString ">"
and isZeroName = Name.fromString "isZero"
and leName = Name.fromString "<="
and ltName = Name.fromString "<"
and modName = Name.fromString "mod"
and multName = Name.fromString "*"
and negName = Name.fromString "~"
and oddName = Name.fromString "odd"
and preName = Name.fromString "pre"
and subName = Name.fromString "-"
and sucName = Name.fromString "suc";;

  (* Support *)

  let modN s x = x mod s.size;;

  let oneN sz = modN sz 1;;

  let multN sz (x,y) = modN sz (x * y);;

  (* Functions *)

  let numeralFn i sz = Some (modN sz i);;

  let addFn sz x y = Some (modN sz (x + y));;

  let divFn s x y =
      let n = s.size in
        let y = if y = 0 then n else y
      in
        Some (Int.div x y)
      ;;

  let expFn sz x y = Some (exp (multN sz) x y (oneN sz));;

  let modFn s x y =
    let n = s.size in
        let y = if y = 0 then n else y
      in
        Some (x mod y)
      ;;

  let multFn sz x y = Some (multN sz (x,y));;

  let negFn n x = Some (if x = 0 then 0 else n.size - x);;

  let preFn n x = Some (if x = 0 then n.size - 1 else x - 1);;

  let subFn n x y = Some (if x < y then n.size + x - y else x - y);;

  let sucFn n x = Some (if x = n.size - 1 then 0 else x + 1);;

  (* Relations *)

  let dividesRel _ x y = Some (divides x y);;

  let evenRel _ x = Some (x mod 2 = 0);;

  let geRel _ x y = Some (x >= y);;

  let gtRel _ x y = Some (x > y);;

  let isZeroRel _ x = Some (x = 0);;

  let leRel _ x y = Some (x <= y);;

  let ltRel _ x y = Some (x < y);;

  let oddRel _ x = Some (x mod 2 = 1);;

  let modularFixed =
        let fns =
            Name_arity.Map.fromList
              (List.map (fun i -> ((numeralName i,0), fixed0 (numeralFn i)))
                 numeralList @
               [((addName,2), fixed2 addFn);
                ((divName,2), fixed2 divFn);
                ((expName,2), fixed2 expFn);
                ((modName,2), fixed2 modFn);
                ((multName,2), fixed2 multFn);
                ((negName,1), fixed1 negFn);
                ((preName,1), fixed1 preFn);
                ((subName,2), fixed2 subFn);
                ((sucName,1), fixed1 sucFn)])

        in let rels =
            Name_arity.Map.fromList
              [((dividesName,2), fixed2 dividesRel);
               ((evenName,1), fixed1 evenRel);
               ((geName,2), fixed2 geRel);
               ((gtName,2), fixed2 gtRel);
               ((isZeroName,1), fixed1 isZeroRel);
               ((leName,2), fixed2 leRel);
               ((ltName,2), fixed2 ltRel);
               ((oddName,1), fixed1 oddRel)]
      in
          {functions = fns;
           relations = rels}
      ;;

  (* Support *)

  let cutN s x =
    let n = s.size in
      if x >= n then n - 1 else x;;

  let oneN sz = cutN sz 1;;

  let multN sz (x,y) = cutN sz (x * y);;

  (* Functions *)

  let numeralFn i sz = if i < 0 then None else Some (cutN sz i);;

  let addFn sz x y = Some (cutN sz (x + y));;

  let divFn _ x y = if y = 0 then None else Some (Int.div x y);;

  let expFn sz x y = Some (exp (multN sz) x y (oneN sz));;

  let modFn n x y =
      if y = 0 || x = n.size - 1 then None else Some (x mod y);;

  let multFn sz x y = Some (multN sz (x,y));;

  let negFn _ x = if x = 0 then Some 0 else None;;

  let preFn _ x = if x = 0 then None else Some (x - 1);;

  let subFn n x y =
      if y = 0 then Some x
      else if x = n.size - 1 || x < y then None
      else Some (x - y);;

  let sucFn sz x = Some (cutN sz (x + 1));;

  (* Relations *)

  let dividesRel n x y =
      if x = 1 || y = 0 then Some true
      else if x = 0 then Some false
      else if y = n.size - 1 then None
      else Some (divides x y);;

  let evenRel n x =
      if x = n.size - 1 then None else Some (x mod 2 = 0);;

  let geRel s y x =
      let n = s.size in
      if x = n - 1 then if y = n - 1 then None else Some false
      else if y = n - 1 then Some true else Some (x <= y);;

  let gtRel s y x =
      let n = s.size in
      if x = n - 1 then if y = n - 1 then None else Some false
      else if y = n - 1 then Some true else Some (x < y);;

  let isZeroRel _ x = Some (x = 0);;

  let leRel s x y =
      let n = s.size in
      if x = n - 1 then if y = n - 1 then None else Some false
      else if y = n - 1 then Some true else Some (x <= y);;

  let ltRel s x y =
      let n = s.size in
      if x = n - 1 then if y = n - 1 then None else Some false
      else if y = n - 1 then Some true else Some (x < y);;

  let oddRel s x =
      let n = s.size in
      if x = n - 1 then None else Some (x mod 2 = 1);;

  let overflowFixed =
        let fns =
            Name_arity.Map.fromList
              (List.map (fun i -> ((numeralName i,0), fixed0 (numeralFn i)))
                 numeralList @
               [((addName,2), fixed2 addFn);
                ((divName,2), fixed2 divFn);
                ((expName,2), fixed2 expFn);
                ((modName,2), fixed2 modFn);
                ((multName,2), fixed2 multFn);
                ((negName,1), fixed1 negFn);
                ((preName,1), fixed1 preFn);
                ((subName,2), fixed2 subFn);
                ((sucName,1), fixed1 sucFn)])

        in let rels =
            Name_arity.Map.fromList
              [((dividesName,2), fixed2 dividesRel);
               ((evenName,1), fixed1 evenRel);
               ((geName,2), fixed2 geRel);
               ((gtName,2), fixed2 gtRel);
               ((isZeroName,1), fixed1 isZeroRel);
               ((leName,2), fixed2 leRel);
               ((ltName,2), fixed2 ltRel);
               ((oddName,1), fixed1 oddRel)]
      in
          {functions = fns;
           relations = rels}
      ;;

(* Sets *)

let cardName = Name.fromString "card"
and complementName = Name.fromString "complement"
and differenceName = Name.fromString "difference"
and emptyName = Name.fromString "empty"
and memberName = Name.fromString "member"
and insertName = Name.fromString "insert"
and intersectName = Name.fromString "intersect"
and singletonName = Name.fromString "singleton"
and subsetName = Name.fromString "subset"
and symmetricDifferenceName = Name.fromString "symmetricDifference"
and unionName = Name.fromString "union"
and universeName = Name.fromString "universe";;

  (* Support *)

  let eltN s =
      let n = s.size in
        let rec f acc = function
            0 -> acc
          | x -> f (acc + 1) (Int.div x 2)
      in
        f (-1) n
      ;;

  let posN i = Word.shiftLeft (1, Word.fromInt i);;

  let univN sz = Word.minus (posN (eltN sz), 1);;

  let setN sz x = Word.andb (Word.fromInt x, univN sz);;

  (* Functions *)

  let cardFn sz x =
        let rec f acc = function
            0 -> acc
          | s ->
              let acc = if Word.andb (s,1) = 0 then acc else acc + 1
            in
              f acc (Word.shiftRight (s,1))
      in
        Some (f (setN sz x) 0)
      ;;

  let complementFn sz x = Some (Word.toInt (Word.xorb (univN sz, setN sz x)));;

  let differenceFn sz x y =
        let x = setN sz x
        and y = setN sz y
      in
        Some (Word.toInt (Word.andb (x, Word.notb y)))
      ;;

  let emptyFn _ = Some 0;;

  let insertFn sz x y =
        let x = x mod eltN sz
        and y = setN sz y
      in
        Some (Word.toInt (Word.orb (posN x, y)))
      ;;

  let intersectFn sz x y =
      Some (Word.toInt (Word.andb (setN sz x, setN sz y)));;

  let singletonFn sz x =
        let x = x mod eltN sz
      in
        Some (Word.toInt (posN x))
      ;;

  let symmetricDifferenceFn sz x y =
        let x = setN sz x
        and y = setN sz y
      in
        Some (Word.toInt (Word.xorb (x,y)))
      ;;

  let unionFn sz x y =
      Some (Word.toInt (Word.orb (setN sz x, setN sz y)));;

  let universeFn sz = Some (Word.toInt (univN sz));;

  (* Relations *)

  let memberRel sz x y =
        let x = x mod eltN sz
        and y = setN sz y
      in
        Some (Word.andb (posN x, y) <> 0)
      ;;

  let subsetRel sz x y =
        let x = setN sz x
        and y = setN sz y
      in
        Some (Word.andb (x, Word.notb y) = 0)
      ;;

  let setFixed =
        let fns =
            Name_arity.Map.fromList
              [((cardName,1), fixed1 cardFn);
               ((complementName,1), fixed1 complementFn);
               ((differenceName,2), fixed2 differenceFn);
               ((emptyName,0), fixed0 emptyFn);
               ((insertName,2), fixed2 insertFn);
               ((intersectName,2), fixed2 intersectFn);
               ((singletonName,1), fixed1 singletonFn);
               ((symmetricDifferenceName,2), fixed2 symmetricDifferenceFn);
               ((unionName,2), fixed2 unionFn);
               ((universeName,0), fixed0 universeFn)]

        in let rels =
            Name_arity.Map.fromList
              [((memberName,2), fixed2 memberRel);
               ((subsetName,2), fixed2 subsetRel)]
      in
          {functions = fns;
           relations = rels}
      ;;

(* Lists *)

let appendName = Name.fromString "@"
and consName = Name.fromString "::"
and lengthName = Name.fromString "length"
and nilName = Name.fromString "nil"
and nullName = Name.fromString "null"
and tailName = Name.fromString "tail";;

  let baseFix =
        let fix = unionFixed projectionFixed overflowFixed

        in let sucFn = getFunctionFixed fix (sucName,1)

        in let suc2Fn sz _ x = sucFn sz [x]
      in
        insertFunctionFixed fix ((sucName,2), fixed2 suc2Fn)
      ;;

  let fixMap =
      {functionMap = Name_arity.Map.fromList
                       [((appendName,2),addName);
                        ((consName,2),sucName);
                        ((lengthName,1), projectionName 1);
                        ((nilName,0), numeralName 0);
                        ((tailName,1),preName)];
       relationMap = Name_arity.Map.fromList
                       [((nullName,1),isZeroName)]};;

  let listFixed = mapFixed fixMap baseFix;;

(* ------------------------------------------------------------------------- *)
(* Valuations.                                                               *)
(* ------------------------------------------------------------------------- *)

type valuation = Valuation of element Name.Map.map;;

let emptyValuation = Valuation (Name.Map.newMap ());;

let insertValuation (Valuation m) v_i = Valuation (Name.Map.insert m v_i);;

let peekValuation (Valuation m) v = Name.Map.peek m v;;

let constantValuation i =
      let add (v,v') = insertValuation v' (v,i)
    in
      Name.Set.foldl add emptyValuation
    ;;

let zeroValuation = constantValuation zeroElement;;

let getValuation v' v =
    match peekValuation v' v with
      Some i -> i
    | None -> raise (Error "Model.getValuation: incomplete valuation");;

let randomValuation s vs =
      let n = s.size in
      let f (v,v') = insertValuation v' (v, Portable.randomInt n)
    in
      Name.Set.foldl f emptyValuation vs
    ;;

let incrementValuation n vars =
      let rec inc vs v' =
          match vs with
            [] -> None
          | v :: vs ->
              let (carry,i) =
                  match incrementElement n (getValuation v' v) with
                    Some i -> (false,i)
                  | None -> (true,zeroElement)

              in let v' = insertValuation v' (v,i)
            in
              if carry then inc vs v' else Some v'
    in
      inc (Name.Set.toList vars)
    ;;

let foldValuation n vars f =
      let inc = incrementValuation n vars

      in let rec fold v' acc =
            let acc = f (v',acc)
          in
            match inc v' with
              None -> acc
            | Some v' -> fold v' acc

      in let zero = zeroValuation vars
    in
      fold zero
    ;;

(* ------------------------------------------------------------------------- *)
(* A type of random finite mapping Z^n -> Z.                                 *)
(* ------------------------------------------------------------------------- *)

let cUNKNOWN = -1;;

type table =
    Forgetful_table
  | Array_table of int array;;

let newTable n arity =
    match elementListSpace {size = n} arity with
      None -> Forgetful_table
    | Some space -> Array_table (Array.make space cUNKNOWN);;


  let randomResult r = Portable.randomInt r;;
  let lookupTable n vR table elts =
      match table with
        Forgetful_table -> randomResult vR
      | Array_table a ->
          let i = elementListIndex {size = n} elts

          in let r = Array.get a i
        in
          if r <> cUNKNOWN then r
          else
              let r = randomResult vR

              in let () = Array.set a i r
            in
              r
        ;;

let updateTable n table (elts,r) =
    match table with
      Forgetful_table -> ()
    | Array_table a ->
        let i = elementListIndex {size = n} elts

        in let () = Array.set a i r
      in
        ()
      ;;

(* ------------------------------------------------------------------------- *)
(* A type of random finite mappings name * arity -> Z^arity -> Z.            *)
(* ------------------------------------------------------------------------- *)

type tables =
      {domainSize : int;
       rangeSize : int;
       tableMap : table Name_arity.Map.map ref};;

let newTables n vR =
      {domainSize = n;
       rangeSize = vR;
       tableMap = ref (Name_arity.Map.newMap ())};;

let getTables tables n_a =
    let n = tables.domainSize in
    let tm = tables.tableMap in
    let m = !tm in
      match Name_arity.Map.peek m n_a with
        Some t -> t
      | None ->
          let (_,a) = n_a

          in let t = newTable n a

          in let m = Name_arity.Map.insert m (n_a,t)

          in let () = tm := m
        in
          t
    ;;

let lookupTables tables (n,elts) =
    let vN = tables.domainSize in
    let vR = tables.rangeSize in
    let a = length elts in
    let table = getTables tables (n,a) in
      lookupTable vN vR table elts
    ;;

let updateTables tables ((n,elts),r) =
    let vN = tables.domainSize in
    let a = length elts in
    let table = getTables tables (n,a) in
      updateTable vN table (elts,r)
    ;;

(* ------------------------------------------------------------------------- *)
(* A type of random finite models.                                           *)
(* ------------------------------------------------------------------------- *)

type parameters = {sizep : int; fixed : fixed};;

type model =
      {sizem : int;
       fixedFunctions : (element list -> element option) Name_arity.Map.map;
       fixedRelations : (element list -> bool option) Name_arity.Map.map;
       randomFunctions : tables;
       randomRelations : tables};;

let newModel x =
    let vN = x.sizep in
    let fixed = x.fixed in
    let fns = fixed.functions in
    let rels = fixed.relations in
    let fixFns = Name_arity.Map.transform (fun f -> f {size = vN}) fns
    and fixRels = Name_arity.Map.transform (fun r -> r {size = vN}) rels

      in let rndFns = newTables vN vN
      and rndRels = newTables vN 2
    in
        {sizem = vN;
         fixedFunctions = fixFns;
         fixedRelations = fixRels;
         randomFunctions = rndFns;
         randomRelations = rndRels}
    ;;

let msize x = x.sizem;;
let psize x = x.sizep;;

let peekFixedFunction vM (n,elts) =
    let fixFns = vM.fixedFunctions in
      match Name_arity.Map.peek fixFns (n, length elts) with
        None -> None
      | Some fixFn -> fixFn elts
    ;;

let isFixedFunction vM n_elts = Option.isSome (peekFixedFunction vM n_elts);;

let peekFixedRelation vM (n,elts) =
    let fixRels = vM.fixedRelations in
      match Name_arity.Map.peek fixRels (n, length elts) with
        None -> None
      | Some fixRel -> fixRel elts
    ;;

let isFixedRelation vM n_elts = Option.isSome (peekFixedRelation vM n_elts);;

(* A default model *)

let defaultSize = 8;;

let defaultFixed =
    unionListFixed
      [basicFixed;
       projectionFixed;
       modularFixed;
       setFixed;
       listFixed];;

let default = {sizep = defaultSize; fixed = defaultFixed};;

(* ------------------------------------------------------------------------- *)
(* Taking apart terms to interpret them.                                     *)
(* ------------------------------------------------------------------------- *)

let destTerm tm =
    match tm with
      Term.Var _ -> tm
    | Term.Fn f_tms ->
      match Term.stripApp tm with
        (_,[]) -> tm
      | (Term.Var _ as v, tms) -> Term.Fn (Term.appName, v :: tms)
      | (Term.Fn (f,tms), tms') -> Term.Fn (f, tms @ tms');;

(* ------------------------------------------------------------------------- *)
(* Interpreting terms and formulas in the model.                             *)
(* ------------------------------------------------------------------------- *)

let interpretFunction vM n_elts =
    match peekFixedFunction vM n_elts with
      Some r -> r
    | None ->
        let rndFns = vM.randomFunctions in
          lookupTables rndFns n_elts
      ;;

let interpretRelation vM n_elts =
    match peekFixedRelation vM n_elts with
      Some r -> r
    | None ->
        let rndRels = vM.randomRelations in
          intToBool (lookupTables rndRels n_elts)
      ;;

let interpretTerm vM vV =
      let rec interpret tm =
          match destTerm tm with
            Term.Var v -> getValuation vV v
          | Term.Fn (f,tms) -> interpretFunction vM (f, List.map interpret tms)
    in
      interpret
    ;;

let interpretAtom vM vV (r,tms) =
    interpretRelation vM (r, List.map (interpretTerm vM vV) tms);;

let interpretFormula vM =
      let vN = msize vM

      in let rec interpret vV fm =
          match fm with
            Formula.True -> true
          | Formula.False -> false
          | Formula.Atom atm -> interpretAtom vM vV atm
          | Formula.Not p -> not (interpret vV p)
          | Formula.Or (p,q) -> interpret vV p || interpret vV q
          | Formula.And (p,q) -> interpret vV p && interpret vV q
          | Formula.Imp (p,q) -> interpret vV (Formula.Or (Formula.Not p, q))
          | Formula.Iff (p,q) -> interpret vV p = interpret vV q
          | Formula.Forall (v,p) -> interpret' vV p v vN
          | Formula.Exists (v,p) ->
            interpret vV (Formula.Not (Formula.Forall (v, Formula.Not p)))

      and interpret' vV fm v i =
          i = 0 ||
            let i = i - 1
            in let vV' = insertValuation vV (v,i)
          in
            interpret vV' fm && interpret' vV fm v i

    in
      interpret
    ;;

let interpretLiteral vM vV (pol,atm) =
      let b = interpretAtom vM vV atm
    in
      if pol then b else not b
    ;;

let interpretClause vM vV cl = Literal.Set.exists (interpretLiteral vM vV) cl;;

(* ------------------------------------------------------------------------- *)
(* Check whether random groundings of a formula are true in the model.       *)
(* Note: if it's cheaper, a systematic check will be performed instead.      *)
(* ------------------------------------------------------------------------- *)

let check interpret maxChecks vM fv x =
      let vN = msize vM

      in let score (vV,(vT,vF)) =
          if interpret vM vV x then (vT + 1, vF) else (vT, vF + 1)

      in let randomCheck acc = score (randomValuation {size = vN} fv, acc)

      in let maxChecks =
          match maxChecks with
            None -> maxChecks
          | Some m ->
            match expInt vN (Name.Set.size fv) with
              Some n -> if n <= m then None else maxChecks
            | None -> maxChecks
    in
      match maxChecks with
        Some m -> funpow m randomCheck (0, 0)
      | None -> foldValuation {size = vN} fv score (0, 0)
    ;;

let checkAtom maxChecks vM atm =
    check interpretAtom maxChecks vM (Atom.freeVars atm) atm;;

let checkFormula maxChecks vM fm =
    check interpretFormula maxChecks vM (Formula.freeVars fm) fm;;

let checkLiteral maxChecks vM lit =
    check interpretLiteral maxChecks vM (Literal.freeVars lit) lit;;

let checkClause maxChecks vM cl =
    check interpretClause maxChecks vM (Literal.Set.freeVars cl) cl;;

(* ------------------------------------------------------------------------- *)
(* Updating the model.                                                       *)
(* ------------------------------------------------------------------------- *)

let updateFunction vM func_elts_elt =
    let rndFns = vM.randomFunctions in
    let () = updateTables rndFns func_elts_elt in
      ()
    ;;

let updateRelation vM (rel_elts,pol) =
    let rndRels = vM.randomRelations in
    let () = updateTables rndRels (rel_elts, boolToInt pol) in
      ()
    ;;

(* ------------------------------------------------------------------------- *)
(* A type of terms with interpretations embedded in the subterms.            *)
(* ------------------------------------------------------------------------- *)

type modelTerm =
    Model_var
  | Model_fn of Term.functionName * modelTerm list * int list;;

let modelTerm vM vV =
      let rec modelTm tm =
          match destTerm tm with
            Term.Var v -> (Model_var, getValuation vV v)
          | Term.Fn (f,tms) ->
              let (tms,xs) = unzip (List.map modelTm tms)
            in
              (Model_fn (f,tms,xs), interpretFunction vM (f,xs))
    in
      modelTm
    ;;

(* ------------------------------------------------------------------------- *)
(* Perturbing the model.                                                     *)
(* ------------------------------------------------------------------------- *)

type perturbation =
    Function_perturbation of (Term.functionName * element list) * element
  | Relation_perturbation of (Atom.relationName * element list) * bool;;

let perturb vM pert =
    match pert with
      Function_perturbation ((func,elts),elt) -> updateFunction vM ((func,elts),elt)
    | Relation_perturbation ((rel,elts),pol) -> updateRelation vM ((rel,elts),pol);;

  let rec pertTerm vM target tm acc =
      match target with [] -> acc | _ ->
      (match tm with
        Model_var -> acc
      | Model_fn (func,tms,xs) ->
          let onTarget ys = mem (interpretFunction vM (func,ys)) target

          in let func_xs = (func,xs)

          in let acc =
              if isFixedFunction vM func_xs then acc
              else
                  let add (y,acc) = Function_perturbation (func_xs,y) :: acc
                in
                  Mlist.foldl add acc target
        in
          pertTerms vM onTarget tms xs acc)

  and pertTerms vM onTarget =
        let vN = msize vM

        in let filterElements pred =
              let rec filt i acc = match i with
                  0 -> acc
                | _ ->
                    let i = i - 1
                    in let acc = if pred i then i :: acc else acc
                  in
                    filt i acc
            in
              filt vN []

        in let rec pert = function
            (_, [], [], acc) -> acc
          | (ys, (tm :: tms), (x :: xs), acc) ->
              let pred y =
                  y <> x && onTarget (Mlist.revAppend (ys, y :: xs))

              in let target = filterElements pred

              in let acc = pertTerm vM target tm acc
            in
              pert ((x :: ys), tms, xs, acc)
          | (_, _, _, _) -> raise (Bug "Model.pertTerms.pert")
      in
        fun x y z -> pert ([],x,y,z)
      ;;

  let pertAtom vM vV target (rel,tms) acc =
        let onTarget ys = interpretRelation vM (rel,ys) = target

        in let (tms,xs) = unzip (List.map (modelTerm vM vV) tms)

        in let rel_xs = (rel,xs)

        in let acc =
            if isFixedRelation vM rel_xs then acc
            else Relation_perturbation (rel_xs,target) :: acc
      in
        pertTerms vM onTarget tms xs acc
      ;;

  let pertLiteral vM vV ((pol,atm),acc) = pertAtom vM vV pol atm acc;;

  let pertClause vM vV cl acc = Literal.Set.foldl (pertLiteral vM vV) acc cl;;

  let pickPerturb vM perts =
      if Mlist.null perts then ()
      else perturb vM (Mlist.nth (perts, Portable.randomInt (length perts)));;

  let perturbTerm vM vV (tm,target) =
      pickPerturb vM (pertTerm vM target (fst (modelTerm vM vV tm)) []);;

  let perturbAtom vM vV (atm,target) =
      pickPerturb vM (pertAtom vM vV target atm []);;

  let perturbLiteral vM vV lit = pickPerturb vM (pertLiteral vM vV (lit,[]));;

  let perturbClause vM vV cl = pickPerturb vM (pertClause vM vV cl []);;


end


(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS              *)
(* ========================================================================= *)

module Term_net = struct

open Useful;;
open Order;;

(* ------------------------------------------------------------------------- *)
(* Anonymous variables.                                                      *)
(* ------------------------------------------------------------------------- *)

let anonymousName = Name.fromString "_";;
let anonymousVar = Term.Var anonymousName;;

(* ------------------------------------------------------------------------- *)
(* Quotient terms.                                                           *)
(* ------------------------------------------------------------------------- *)

type qterm =
    Var
  | Fn of Name_arity.nameArity * qterm list;;

  let rec cmp = function
      [] -> Equal
    | (q1_q2 :: qs) ->
      if Portable.pointerEqual q1_q2 then cmp qs
      else
        match q1_q2 with
          (Var,Var) -> Equal
        | (Var, Fn _) -> Less
        | (Fn _, Var) -> Greater
        | (Fn (f1, f1'), Fn (f2, f2')) -> fnCmp (f1,f1') (f2,f2') qs

  and fnCmp (n1,q1) (n2,q2) qs =
    match Name_arity.compare (n1,n2) with
      Less -> Less
    | Equal -> cmp (zip q1 q2 @ qs)
    | Greater -> Greater;;

  let compareQterm q1_q2 = cmp [q1_q2];;

  let compareFnQterm (f1,f2) = fnCmp f1 f2 [];;


let equalQterm q1 q2 = compareQterm (q1,q2) = Equal;;

let equalFnQterm f1 f2 = compareFnQterm (f1,f2) = Equal;;

let rec termToQterm = function
    (Term.Var _) -> Var
  | (Term.Fn (f,l)) -> Fn ((f, length l), List.map termToQterm l);;

  let rec qm = function
      [] -> true
    | ((Var,_) :: rest) -> qm rest
    | ((Fn _, Var) :: _) -> false
    | ((Fn (f,a), Fn (g,b)) :: rest) ->
      Name_arity.equal f g && qm (zip a b @ rest);;

  let matchQtermQterm qtm qtm' = qm [(qtm,qtm')];;

  let rec qm = function
      [] -> true
    | ((Var,_) :: rest) -> qm rest
    | ((Fn _, Term.Var _) :: _) -> false
    | ((Fn ((f,n),a), Term.Fn (g,b)) :: rest) ->
      Name.equal f g && n = length b && qm (zip a b @ rest);;

  let matchQtermTerm qtm tm = qm [(qtm,tm)];;

  let rec qn qsub = function
      [] -> Some qsub
    | ((Term.Var v, qtm) :: rest) ->
      (match Name.Map.peek qsub v with
         None -> qn (Name.Map.insert qsub (v,qtm)) rest
       | Some qtm' -> if equalQterm qtm qtm' then qn qsub rest else None)
    | ((Term.Fn _, Var) :: _) -> None
    | ((Term.Fn (f,a), Fn ((g,n),b)) :: rest) ->
      if Name.equal f g && length a = n then qn qsub (zip a b @ rest)
      else None;;

  let matchTermQterm qsub tm qtm = qn qsub [(tm,qtm)];;

  let rec qv s t = match (s,t) with
      (Var, x) -> x
    | (x, Var) -> x
    | (Fn (f,a), Fn (g,b)) ->
        let _ = Name_arity.equal f g || raise (Error "Term_net.qv")
      in
        Fn (f, zipWith qv a b)
      ;;

  let rec qu qsub = function
      [] -> qsub
    | ((Var, _) :: rest) -> qu qsub rest
    | ((qtm, Term.Var v) :: rest) ->
        let qtm =
            match Name.Map.peek qsub v with None -> qtm | Some qtm' -> qv qtm qtm'
      in
        qu (Name.Map.insert qsub (v,qtm)) rest
    | ((Fn ((f,n),a), Term.Fn (g,b)) :: rest) ->
      if Name.equal f g && n = length b then qu qsub (zip a b @ rest)
      else raise (Error "Term_net.qu");;

  let unifyQtermQterm qtm qtm' = total (qv qtm) qtm';;

  let unifyQtermTerm qsub qtm tm = total (qu qsub) [(qtm,tm)];;

  let rec qtermToTerm = function
      Var -> anonymousVar
    | (Fn ((f,_),l)) -> Term.Fn (f, List.map qtermToTerm l);;


(* ------------------------------------------------------------------------- *)
(* A type of term sets that can be efficiently matched and unified.          *)
(* ------------------------------------------------------------------------- *)

type parameters = {fifo : bool};;

type 'a net =
    Result of 'a list
  | Single of qterm * 'a net
  | Multiple of 'a net option * 'a net Name_arity.Map.map;;

type 'a termNet = Net of parameters * int * (int * (int * 'a) net) option;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let newNet parm = Net (parm,0,None);;

  let rec computeSize = function
      (Result l) -> length l
    | (Single (_,n)) -> computeSize n
    | (Multiple (vs,fs)) ->
      Name_arity.Map.foldl
        (fun (_,n,acc) -> acc + computeSize n)
        (match vs with Some n -> computeSize n | None -> 0)
        fs;;

  let netSize = function
      None -> None
    | (Some n) -> Some (computeSize n, n);;


let size = function
    (Net (_,_,None)) -> 0
  | (Net (_, _, Some (i,_))) -> i;;

let null net = size net = 0;;

let singles qtms a = Mlist.foldr (fun (x, y) -> Single (x, y)) a qtms;;

  let pre = function
      None -> (0,None)
    | (Some (i,n)) -> (i, Some n);;

  let rec add a b c = match (a, b, c) with
      (Result l, [], Result l') -> Result (l @ l')
    | (a, (qtm :: qtms as input1), Single (qtm',n)) ->
      if equalQterm qtm qtm' then Single (qtm, add a qtms n)
      else add a input1 (add n [qtm'] (Multiple (None, Name_arity.Map.newMap ())))
    | (a, Var :: qtms, Multiple (vs,fs)) ->
      Multiple (Some (oadd a qtms vs), fs)
    | (a, Fn (f,l) :: qtms, Multiple (vs,fs)) ->
        let n = Name_arity.Map.peek fs f
      in
        Multiple (vs, Name_arity.Map.insert fs (f, oadd a (l @ qtms) n))
    | _ -> raise (Bug "Term_net.insert: Match")

  and oadd a qtms = function
      None -> singles qtms a
    | (Some n) -> add a qtms n;;

  let ins a qtm (i,n) = Some (i + 1, oadd (Result [a]) [qtm] n);;

  let insert (Net (p,k,n)) (tm,a) =
      try Net (p, k + 1, ins (k,a) (termToQterm tm) (pre n))
      with Error _ -> raise (Bug "Term_net.insert: should never fail");;


let fromList parm l = Mlist.foldl (fun (tm_a,n) -> insert n tm_a) (newNet parm) l;;

let filter pred =
      let rec filt = function
          (Result l) ->
          (match List.filter (fun (_,a) -> pred a) l with
             [] -> None
           | l -> Some (Result l))
        | (Single (qtm,n)) ->
          (match filt n with
             None -> None
           | Some n -> Some (Single (qtm,n)))
        | (Multiple (vs,fs)) ->
            let vs = Option.mapPartial filt vs

            in let fs = Name_arity.Map.mapPartial (fun (_,n) -> filt n) fs
          in
            if not (Option.isSome vs) && Name_arity.Map.null fs then None
            else Some (Multiple (vs,fs))
    in try
      function
         Net (_,_,None) as net -> net
       | Net (p, k, Some (_,n)) -> Net (p, k, netSize (filt n))
    with Error _ -> raise (Bug "Term_net.filter: should never fail");;

let toString net = "Term_net[" ^ Int.toString (size net) ^ "]";;

(* ------------------------------------------------------------------------- *)
(* Specialized fold operations to support matching and unification.          *)
(* ------------------------------------------------------------------------- *)

  let rec norm = function
      (0 :: ks, ((_,n) as f) :: fs, qtms) ->
        let (a,qtms) = revDivide qtms n
      in
        addQterm (Fn (f,a)) (ks,fs,qtms)
    | stack -> stack

  and addQterm qtm (ks,fs,qtms) =
        let ks = match ks with [] -> [] | k :: ks -> (k - 1) :: ks
      in
        norm (ks, fs, qtm :: qtms)

  and addFn ((_,n) as f) (ks,fs,qtms) = norm (n :: ks, f :: fs, qtms);;

  let stackEmpty = ([],[],[]);;

  let stackAddQterm = addQterm;;

  let stackAddFn = addFn;;

  let stackValue = function
      ([],[],[qtm]) -> qtm
    | _ -> raise (Bug "Term_net.stackValue");;


  let rec fold inc acc = function
      [] -> acc
    | ((0,stack,net) :: rest) ->
      fold inc (inc (stackValue stack, net, acc)) rest
    | ((n, stack, Single (qtm,net)) :: rest) ->
      fold inc acc ((n - 1, stackAddQterm qtm stack, net) :: rest)
    | ((n, stack, Multiple (v,fns)) :: rest) ->
        let n = n - 1

        in let rest =
            match v with
              None -> rest
            | Some net -> (n, stackAddQterm Var stack, net) :: rest

        in let getFns ((_,k) as f, net, x) =
            (k + n, stackAddFn f stack, net) :: x
      in
        fold inc acc (Name_arity.Map.foldr getFns rest fns)
    | _ -> raise (Bug "Term_net.foldTerms.fold");;

  let foldTerms inc acc net = fold inc acc [(1,stackEmpty,net)];;


let foldEqualTerms pat inc acc =
      let rec fold = function
          ([],net) -> inc (pat,net,acc)
        | (pat :: pats, Single (qtm,net)) ->
          if equalQterm pat qtm then fold (pats,net) else acc
        | (Var :: pats, Multiple (v,_)) ->
          (match v with None -> acc | Some net -> fold (pats,net))
        | (Fn (f,a) :: pats, Multiple (_,fns)) ->
          (match Name_arity.Map.peek fns f with
             None -> acc
           | Some net -> fold (a @ pats, net))
        | _ -> raise (Bug "Term_net.foldEqualTerms.fold")
    in
      fun net -> fold ([pat],net)
    ;;


  let rec fold inc acc = function
      [] -> acc
    | (([],stack,net) :: rest) ->
      fold inc (inc (stackValue stack, net, acc)) rest
    | ((Var :: pats, stack, net) :: rest) ->
        let harvest (qtm,n,l) = (pats, stackAddQterm qtm stack, n) :: l
      in
        fold inc acc (foldTerms harvest rest net)
    | ((pat :: pats, stack, Single (qtm,net)) :: rest) ->
      (match unifyQtermQterm pat qtm with
         None -> fold inc acc rest
       | Some qtm ->
         fold inc acc ((pats, stackAddQterm qtm stack, net) :: rest))
    | (((Fn (f,a) as pat) :: pats, stack, Multiple (v,fns)) :: rest) ->
        let rest =
            match v with
              None -> rest
            | Some net -> (pats, stackAddQterm pat stack, net) :: rest

        in let rest =
            match Name_arity.Map.peek fns f with
              None -> rest
            | Some net -> (a @ pats, stackAddFn f stack, net) :: rest
      in
        fold inc acc rest
    | _ -> raise (Bug "Term_net.foldUnifiableTerms.fold");;

  let foldUnifiableTerms pat inc acc net =
      fold inc acc [([pat],stackEmpty,net)];;

(* ------------------------------------------------------------------------- *)
(* Matching and unification queries.                                         *)
(*                                                                           *)
(* These function return OVER-APPROXIMATIONS!                                *)
(* Filter afterwards to get the precise set of satisfying values.            *)
(* ------------------------------------------------------------------------- *)

  let idwise ((m,_),(n,_)) = Int.compare (m,n);;

  let fifoize (p : parameters) l = if p.fifo then sort idwise l else l;;

  let finally parm l = List.map snd (fifoize parm l);;


  let rec mat acc = function
      [] -> acc
    | ((Result l, []) :: rest) -> mat (l @ acc) rest
    | ((Single (qtm,n), tm :: tms) :: rest) ->
      mat acc (if matchQtermTerm qtm tm then (n,tms) :: rest else rest)
    | ((Multiple (vs,fs), tm :: tms) :: rest) ->
        let rest = match vs with None -> rest | Some n -> (n,tms) :: rest

        in let rest =
            match tm with
              Term.Var _ -> rest
            | Term.Fn (f,l) ->
              match Name_arity.Map.peek fs (f, length l) with
                None -> rest
              | Some n -> (n, l @ tms) :: rest
      in
        mat acc rest
    | _ -> raise (Bug "Term_net.match: Match");;

  let matchNet x y = match (x,y) with
      (Net (_,_,None), _) -> []
    | (Net (p, _, Some (_,n)), tm) ->
      try finally p (mat [] [(n,[tm])])
      with Error _ -> raise (Bug "Term_net.match: should never fail");;


  let unseenInc qsub v tms (qtm,net,rest) =
      (Name.Map.insert qsub (v,qtm), net, tms) :: rest;;

  let seenInc qsub tms (_,net,rest) = (qsub,net,tms) :: rest;;

  let rec mat acc = function
      [] -> acc
    | ((_, Result l, []) :: rest) -> mat (l @ acc) rest
    | ((qsub, Single (qtm,net), tm :: tms) :: rest) ->
      (match matchTermQterm qsub tm qtm with
         None -> mat acc rest
       | Some qsub -> mat acc ((qsub,net,tms) :: rest))
    | ((qsub, (Multiple _ as net), Term.Var v :: tms) :: rest) ->
      (match Name.Map.peek qsub v with
         None -> mat acc (foldTerms (unseenInc qsub v tms) rest net)
       | Some qtm -> mat acc (foldEqualTerms qtm (seenInc qsub tms) rest net))
    | ((qsub, Multiple (_,fns), Term.Fn (f,a) :: tms) :: rest) ->
        let rest =
            match Name_arity.Map.peek fns (f, length a) with
              None -> rest
            | Some net -> (qsub, net, a @ tms) :: rest
      in
        mat acc rest
    | _ -> raise (Bug "Term_net.matched.mat");;

  let matched x tm = match x with
      (Net (_,_,None)) -> []
    | (Net (parm, _, Some (_,net))) ->
      try finally parm (mat [] [(Name.Map.newMap (), net, [tm])])
      with Error _ -> raise (Bug "Term_net.matched: should never fail");;


  let inc qsub v tms (qtm,net,rest) =
      (Name.Map.insert qsub (v,qtm), net, tms) :: rest;;

  let rec mat acc = function
      [] -> acc
    | ((_, Result l, []) :: rest) -> mat (l @ acc) rest
    | ((qsub, Single (qtm,net), tm :: tms) :: rest) ->
      (match unifyQtermTerm qsub qtm tm with
         None -> mat acc rest
       | Some qsub -> mat acc ((qsub,net,tms) :: rest))
    | ((qsub, (Multiple _ as net), Term.Var v :: tms) :: rest) ->
      (match Name.Map.peek qsub v with
         None -> mat acc (foldTerms (inc qsub v tms) rest net)
       | Some qtm -> mat acc (foldUnifiableTerms qtm (inc qsub v tms) rest net))
    | ((qsub, Multiple (v,fns), Term.Fn (f,a) :: tms) :: rest) ->
        let rest = match v with None -> rest | Some net -> (qsub,net,tms) :: rest

        in let rest =
            match Name_arity.Map.peek fns (f, length a) with
              None -> rest
            | Some net -> (qsub, net, a @ tms) :: rest
      in
        mat acc rest
    | _ -> raise (Bug "Term_net.unify.mat");;

  let unify x tm = match x with
      (Net (_,_,None)) -> []
    | (Net (parm, _, Some (_,net))) ->
      try finally parm (mat [] [(Name.Map.newMap (), net, [tm])])
      with Error _ -> raise (Bug "Term_net.unify: should never fail");;

end


(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
(* ========================================================================= *)

module Atom_net = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

let atomToTerm atom = Term.Fn atom;;

let termToAtom = function
    (Term.Var _) -> raise (Bug "Atom_net.termToAtom")
  | (Term.Fn atom) -> atom;;

(* ------------------------------------------------------------------------- *)
(* A type of atom sets that can be efficiently matched and unified.          *)
(* ------------------------------------------------------------------------- *)

type parameters = Term_net.parameters;;

type 'a atomNet = 'a Term_net.termNet;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let newNet = Term_net.newNet;;

let size = Term_net.size;;

let insert net (atm,a) = Term_net.insert net (atomToTerm atm, a);;

let fromList parm l = Mlist.foldl (fun (atm_a,n) -> insert n atm_a) (newNet parm) l;;

let filter = Term_net.filter;;

let toString net = "Atom_net[" ^ Int.toString (size net) ^ "]";;


(* ------------------------------------------------------------------------- *)
(* Matching and unification queries.                                         *)
(*                                                                           *)
(* These function return OVER-APPROXIMATIONS!                                *)
(* Filter afterwards to get the precise set of satisfying values.            *)
(* ------------------------------------------------------------------------- *)

let matchNet net atm = Term_net.matchNet net (atomToTerm atm);;

let matched net atm = Term_net.matched net (atomToTerm atm);;

let unify net atm = Term_net.unify net (atomToTerm atm);;


end


(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
(* ========================================================================= *)

module Literal_net = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* A type of literal sets that can be efficiently matched and unified.       *)
(* ------------------------------------------------------------------------- *)

type parameters = Atom_net.parameters;;

type 'a literalNet =
    {positive : 'a Atom_net.atomNet;
     negative : 'a Atom_net.atomNet};;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let newNet parm = {positive = Atom_net.newNet parm; negative = Atom_net.newNet parm};;

  let pos (x : 'a literalNet) = Atom_net.size x.positive;;

  let neg (x : 'a literalNet) = Atom_net.size x.negative;;

  let size net = pos net + neg net;;

  (*let profile net = {positiveN = pos net; negativeN = neg net};;*)


let insert x = function
    ((true,atm),a) ->
    {positive = Atom_net.insert x.positive (atm,a); negative = x.negative}
  | ((false,atm),a) ->
    {positive = x.positive; negative = Atom_net.insert x.negative (atm,a)};;

let fromList parm l = Mlist.foldl (fun (lit_a,n) -> insert n lit_a) (newNet parm) l;;

let filter pred x =
    {positive = Atom_net.filter pred x.positive;
     negative = Atom_net.filter pred x.negative};;

let toString net = "Literal_net[" ^ Int.toString (size net) ^ "]";;


(* ------------------------------------------------------------------------- *)
(* Matching and unification queries.                                         *)
(*                                                                           *)
(* These function return OVER-APPROXIMATIONS!                                *)
(* Filter afterwards to get the precise set of satisfying values.            *)
(* ------------------------------------------------------------------------- *)

let matchNet (x : 'a literalNet) = function
    (true,atm) -> Atom_net.matchNet x.positive atm
  | (false,atm) -> Atom_net.matchNet x.negative atm;;

let matched (x : 'a literalNet) = function
    (true,atm) -> Atom_net.matched x.positive atm
  | (false,atm) -> Atom_net.matched x.negative atm;;

let unify (x : 'a literalNet) = function
    (true,atm) -> Atom_net.unify x.positive atm
  | (false,atm) -> Atom_net.unify x.negative atm;;

end


(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES                        *)
(* ========================================================================= *)

module Subsume = struct

open Useful;;
open Order;;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

let findRest pred =
      let rec f ys = function
          [] -> None
        | (x :: xs) ->
          if pred x then Some (x, Mlist.revAppend (ys,xs)) else f (x :: ys) xs
    in
      f []
    ;;

  let addSym (lit,acc) =
      match total Literal.sym lit with
        None -> acc
      | Some lit -> lit :: acc
  let clauseSym lits = Mlist.foldl addSym lits lits;;


let sortClause cl =
      let lits = Literal.Set.toList cl
    in
      sortMap Literal.typedSymbols (revCompare Int.compare) lits
    ;;

let incompatible lit =
      let lits = clauseSym [lit]
    in
      fun lit' -> not (List.exists (can (Literal.unify Substitute.empty lit')) lits)
    ;;

(* ------------------------------------------------------------------------- *)
(* Clause ids and lengths.                                                   *)
(* ------------------------------------------------------------------------- *)

type clauseId = int;;

type clauseLength = int;;

  type idSet = (clauseId * clauseLength) Pset.set;;

  let idCompare ((id1,len1),(id2,len2)) =
      match Int.compare (len1,len2) with
        Less -> Less
      | Equal -> Int.compare (id1,id2)
      | Greater -> Greater;;

  let idSetEmpty : idSet = Pset.empty idCompare;;

  let idSetAdd (id_len,set) : idSet = Pset.add set id_len;;

  let idSetAddMax max ((_,len) as id_len, set) : idSet =
      if len <= max then Pset.add set id_len else set;;

  let idSetIntersect set1 set2 : idSet = Pset.intersect set1 set2;;

(* ------------------------------------------------------------------------- *)
(* A type of clause sets that supports efficient subsumption checking.       *)
(* ------------------------------------------------------------------------- *)

type 'a nonunit_t =
         {nextId : clauseId;
          clauses : (Literal.literal list * Thm.clause * 'a) Intmap.map;
          fstLits : (clauseId * clauseLength) Literal_net.literalNet;
          sndLits : (clauseId * clauseLength) Literal_net.literalNet};;

type 'a subsume =
      {empty : (Thm.clause * Substitute.subst * 'a) list;
       unitn : (Literal.literal * Thm.clause * 'a)  Literal_net.literalNet;
       nonunit : 'a nonunit_t};;

open Term_net
let newSubsume () =
      {empty = [];
       unitn = Literal_net.newNet {fifo = false};
       nonunit =
         {nextId = 0;
          clauses = Intmap.newMap ();
          fstLits = Literal_net.newNet {fifo = false};
          sndLits = Literal_net.newNet {fifo = false}}};;

let size x =
    length x.empty + Literal_net.size x.unitn + Intmap.size x.nonunit.clauses;;

let insert z (cl',a) =
  let empty = z.empty in
  let unitn = z.unitn in
  let nonunit = z.nonunit in
    match sortClause cl' with
      [] ->
        let empty = (cl',Substitute.empty,a) :: empty
      in
        {empty = empty; unitn = unitn; nonunit = nonunit}
    | [lit] ->
        let unitn = Literal_net.insert unitn (lit,(lit,cl',a))
      in
        {empty = empty; unitn = unitn; nonunit = nonunit}
    | fstLit :: (sndLit :: otherLits as nonFstLits) ->
        let nextId = nonunit.nextId in
        let clauses = nonunit.clauses in
        let fstLits = nonunit.fstLits in
        let sndLits = nonunit.sndLits
        in let id_length = (nextId, Literal.Set.size cl')
        in let fstLits = Literal_net.insert fstLits (fstLit,id_length)
        in let (sndLit,otherLits) =
            match findRest (incompatible fstLit) nonFstLits with
              Some sndLit_otherLits -> sndLit_otherLits
            | None -> (sndLit,otherLits)
        in let sndLits = Literal_net.insert sndLits (sndLit,id_length)
        in let lits' = otherLits @ [fstLit;sndLit]
        in let clauses = Intmap.insert clauses (nextId,(lits',cl',a))
        in let nextId = nextId + 1
        in let nonunit = {nextId = nextId; clauses = clauses;
                       fstLits = fstLits; sndLits = sndLits}
      in
        {empty = empty; unitn = unitn; nonunit = nonunit}
      ;;

let filter pred z =
  let empty = z.empty in
  let unitn = z.unitn in
  let nonunit = z.nonunit in
      let pred3 (_,_,x) = pred x
      in let empty = List.filter pred3 empty

      in let unitn = Literal_net.filter pred3 unitn

      in let nonunit =
           let nextId = nonunit.nextId in
           let clauses = nonunit.clauses in
           let fstLits = nonunit.fstLits in
           let sndLits = nonunit.sndLits in
           let clauses' = Intmap.filter (fun x -> pred3 (snd x)) clauses in
             if Intmap.size clauses = Intmap.size clauses' then nonunit
             else
                let predId (id,_) = Intmap.inDomain id clauses'
                in let fstLits = Literal_net.filter predId fstLits
                and sndLits = Literal_net.filter predId sndLits
              in
                {nextId = nextId; clauses = clauses';
                 fstLits = fstLits; sndLits = sndLits}
    in
      {empty = empty; unitn = unitn; nonunit = nonunit}
    ;;

let toString subsume = "Subsume{" ^ Int.toString (size subsume) ^ "}";;


(* ------------------------------------------------------------------------- *)
(* Subsumption checking.                                                     *)
(* ------------------------------------------------------------------------- *)

  let matchLit lit' (lit,acc) =
      match total (Literal.matchLiterals Substitute.empty lit') lit with
        Some sub -> sub :: acc
      | None -> acc;;

  let genClauseSubsumes pred cl' lits' cl a =
        let rec mkSubsl acc sub = function
            [] -> Some (sub, sortMap length Int.compare acc)
          | (lit' :: lits') ->
            match Mlist.foldl (matchLit lit') [] cl with
              [] -> None
            | [sub'] ->
              (match total (Substitute.union sub) sub' with
                 None -> None
               | Some sub -> mkSubsl acc sub lits')
            | subs -> mkSubsl (subs :: acc) sub lits'

        in let rec search = function
            [] -> None
          | ((sub,[]) :: others) ->
              let x = (cl',sub,a)
            in
              if pred x then Some x else search others
          | ((_, [] :: _) :: others) -> search others
          | ((sub, (sub' :: subs) :: subsl) :: others) ->
              let others = (sub, subs :: subsl) :: others
            in
              match total (Substitute.union sub) sub' with
                None -> search others
              | Some sub -> search ((sub,subsl) :: others)
      in
        match mkSubsl [] Substitute.empty lits' with
          None -> None
        | Some sub_subsl -> search [sub_subsl]
      ;;


  let emptySubsumes pred empty = Mlist.find pred empty;;

  let unitSubsumes pred unitn =
        let subLit lit =
              let subUnit (lit',cl',a) =
                  match total (Literal.matchLiterals Substitute.empty lit') lit with
                    None -> None
                  | Some sub ->
                      let x = (cl',sub,a)
                    in
                      if pred x then Some x else None
            in
              first subUnit (Literal_net.matchNet unitn lit)
      in
        first subLit
      ;;

  let nonunitSubsumes pred nonunit max cl =
        let addId = match max with None -> idSetAdd | Some n -> idSetAddMax n

        in let subLit lits (lit,acc) =
            Mlist.foldl addId acc (Literal_net.matchNet lits lit) in

        let clauses = nonunit.clauses in
        let fstLits = nonunit.fstLits in
        let sndLits = nonunit.sndLits in

        let subCl' (id,_) =
              let (lits',cl',a) = Intmap.get clauses id
            in
              genClauseSubsumes pred cl' lits' cl a

        in let fstCands = Mlist.foldl (subLit fstLits) idSetEmpty cl
        in let sndCands = Mlist.foldl (subLit sndLits) idSetEmpty cl
        in let cands = idSetIntersect fstCands sndCands
      in
        Pset.firstl subCl' cands
      ;;

  let genSubsumes pred z max cl =
    let empty = z.empty in
    let unitn = z.unitn in
    let nonunit = z.nonunit in
      match emptySubsumes pred empty with
        (Some _) as s -> s
      | None ->
        if max = Some 0 then None
        else
            let cl = clauseSym (Literal.Set.toList cl)
          in
            match unitSubsumes pred unitn cl with
              Some _ as s -> s
            | None ->
              if max = Some 1 then None
              else nonunitSubsumes pred nonunit max cl
          ;;

  let subsumes pred subsume cl = genSubsumes pred subsume None cl;;

  let strictlySubsumes pred subsume cl =
      genSubsumes pred subsume (Some (Literal.Set.size cl)) cl;;

(*MetisTrace4
let subsumes = fun pred -> fun subsume -> fun cl ->
    let
      let ppCl = Literal.Set.pp
      let ppSub = Substitute.pp
      let () = Print.trace ppCl "Subsume.subsumes: cl" cl
      let result = subsumes pred subsume cl
      let () =
          match result with
            None -> trace "Subsume.subsumes: not subsumed\n"
          | Some (cl,sub,_) ->
            (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl;;
             Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
    in
      result
    end;;

let strictlySubsumes = fun pred -> fun subsume -> fun cl ->
    let
      let ppCl = Literal.Set.pp
      let ppSub = Substitute.pp
      let () = Print.trace ppCl "Subsume.strictlySubsumes: cl" cl
      let result = strictlySubsumes pred subsume cl
      let () =
          match result with
            None -> trace "Subsume.subsumes: not subsumed\n"
          | Some (cl,sub,_) ->
            (Print.trace ppCl "Subsume.subsumes: subsuming cl" cl;;
             Print.trace ppSub "Subsume.subsumes: subsuming sub" sub)
    in
      result
    end;;
*)

let isSubsumed subs cl = Option.isSome (subsumes (kComb true) subs cl);;

let isStrictlySubsumed subs cl =
    Option.isSome (strictlySubsumes (kComb true) subs cl);;

(* ------------------------------------------------------------------------- *)
(* Single clause versions.                                                   *)
(* ------------------------------------------------------------------------- *)

let clauseSubsumes cl' cl =
      let lits' = sortClause cl'
      and lits = clauseSym (Literal.Set.toList cl)
    in
      match genClauseSubsumes (kComb true) cl' lits' lits () with
        Some (_,sub,()) -> Some sub
      | None -> None
    ;;

let clauseStrictlySubsumes cl' cl =
    if Literal.Set.size cl' > Literal.Set.size cl then None
    else clauseSubsumes cl' cl;;

end


(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS                                    *)
(* ========================================================================= *)

module Knuth_bendix_order = struct

open Useful;;
open Order;;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

let notEqualTerm (x,y) = not (Term.equal x y);;

let firstNotEqualTerm f l =
    match Mlist.find notEqualTerm l with
      Some (x,y) -> f x y
    | None -> raise (Bug "firstNotEqualTerm");;

(* ------------------------------------------------------------------------- *)
(* The weight of all constants must be at least 1, and there must be at most *)
(* one unary function with weight 0.                                         *)
(* ------------------------------------------------------------------------- *)

type kbo =
     {weight : Term.function_t -> int;
      precedence : Term.function_t * Term.function_t -> order};;

(* Default weight = uniform *)

let uniformWeight : Term.function_t -> int = kComb 1;;

(* Default precedence = by arity *)

let arityPrecedence : Term.function_t * Term.function_t -> order =
    fun ((f1,n1),(f2,n2)) ->
       match Int.compare (n1,n2) with
         Less -> Less
       | Equal -> Name.compare (f1,f2)
       | Greater -> Greater;;

(* The default order *)

let default = {weight = uniformWeight; precedence = arityPrecedence};;

(* ------------------------------------------------------------------------- *)
(* Term weight-1 represented as a linear function of the weight-1 of the     *)
(* variables in the term (plus a constant).                                  *)
(*                                                                           *)
(* Note that the conditions on weight functions ensure that all weights are  *)
(* at least 1, so all weight-1s are at least 0.                              *)
(* ------------------------------------------------------------------------- *)

type weight = Weight of int Name.Map.map * int;;

let weightEmpty : int Name.Map.map = Name.Map.newMap ();;

let weightZero = Weight (weightEmpty,0);;

let weightIsZero (Weight (m,c)) = c = 0 && Name.Map.null m;;

let weightNeg (Weight (m,c)) = Weight (Name.Map.transform (fun x -> -x) m, -c);;

  let add ((_,n1),(_,n2)) =
        let n = n1 + n2
      in
        if n = 0 then None else Some n
      ;;
  let weightAdd (Weight (m1,c1)) (Weight (m2,c2)) =
      Weight (Name.Map.union add m1 m2, c1 + c2);;

let weightSubtract w1 w2 = weightAdd w1 (weightNeg w2);;

let weightTerm weight =
      let rec wt m c = function
          [] -> Weight (m,c)
        | (Term.Var v :: tms) ->
            let n = Option.getOpt (Name.Map.peek m v, 0)
          in
            wt (Name.Map.insert m (v, n + 1)) (c + 1) tms
        | (Term.Fn (f,a) :: tms) ->
          wt m (c + weight (f, length a)) (a @ tms)
    in
      fun tm -> wt weightEmpty (-1) [tm]
    ;;

let weightLowerBound (Weight (m,c)) =
    if Name.Map.exists (fun (_,n) -> n < 0) m then None else Some c;;

(* ------------------------------------------------------------------------- *)
(* The Knuth-Bendix term order.                                              *)
(* ------------------------------------------------------------------------- *)

let compare x =
      let weight = x.weight in
      let precedence = x.precedence in
      let weightDifference tm1 tm2 =
            let w1 = weightTerm weight tm1
            and w2 = weightTerm weight tm2
          in
            weightSubtract w2 w1

      in let rec weightLess tm1 tm2 =
            let w = weightDifference tm1 tm2
          in
            if weightIsZero w then precedenceLess tm1 tm2
            else weightDiffLess w tm1 tm2

      and weightDiffLess w tm1 tm2 =
          match weightLowerBound w with
            None -> false
          | Some 0 -> precedenceLess tm1 tm2
          | Some n -> n > 0

      and precedenceLess x y = match (x,y) with
          (Term.Fn (f1,a1), Term.Fn (f2,a2)) ->
          (match precedence ((f1, length a1), (f2, length a2)) with
             Less -> true
           | Equal -> firstNotEqualTerm weightLess (zip a1 a2)
           | Greater -> false)
        | _ -> false

      in let weightDiffGreater w tm1 tm2 = weightDiffLess (weightNeg w) tm2 tm1

      in let rec weightCmp tm1 tm2 =
            let w = weightDifference tm1 tm2
          in
            if weightIsZero w then precedenceCmp tm1 tm2
            else if weightDiffLess w tm1 tm2 then Some Less
            else if weightDiffGreater w tm1 tm2 then Some Greater
            else None

      and precedenceCmp x y = match (x,y) with
          (Term.Fn (f1,a1), Term.Fn (f2,a2)) ->
          (match precedence ((f1, length a1), (f2, length a2)) with
             Less -> Some Less
           | Equal -> firstNotEqualTerm weightCmp (zip a1 a2)
           | Greater -> Some Greater)
        | _ -> raise (Bug "kboOrder.precendenceCmp")
    in
      fun (tm1,tm2) ->
         if Term.equal tm1 tm2 then Some Equal else weightCmp tm1 tm2
    ;;

(*MetisTrace7
let compare = fun kbo -> fun (tm1,tm2) ->
    let
      let () = Print.trace Term.pp "Knuth_bendix_order.compare: tm1" tm1
      let () = Print.trace Term.pp "Knuth_bendix_order.compare: tm2" tm2
      let result = compare kbo (tm1,tm2)
      let () =
          match result with
            None -> trace "Knuth_bendix_order.compare: result = Incomparable\n"
          | Some x ->
            Print.trace Print.ppOrder "Knuth_bendix_order.compare: result" x
    in
      result
    end;;
*)

end


(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS                                   *)
(* ========================================================================= *)

module Rewrite = struct

open Useful;;
open Order;;

(* ------------------------------------------------------------------------- *)
(* Orientations of equations.                                                *)
(* ------------------------------------------------------------------------- *)

type orient = Left_to_right | Right_to_left;;

let toStringOrient ort =
    match ort with
      Left_to_right -> "-->"
    | Right_to_left -> "<--";;


let toStringOrientOption orto =
    match orto with
      Some ort -> toStringOrient ort
    | None -> "<->";;


(* ------------------------------------------------------------------------- *)
(* A type of rewrite systems.                                                *)
(* ------------------------------------------------------------------------- *)

type reductionOrder = Term.term * Term.term -> order option;;

type equationId = int;;

type equation = Rule.equation;;

type rewrite_t =
      {order : reductionOrder;
       known : (equation * orient option) Intmap.map;
       redexes : (equationId * orient) Term_net.termNet;
       subterms : (equationId * bool * Term.path) Term_net.termNet;
       waiting : Intset.set};;

type rewrite =
    Rewrite of rewrite_t;;

let updateWaiting rw waiting =
    let Rewrite r = rw in
    let order = r.order in
    let known = r.known in
    let redexes = r.redexes in
    let subterms = r.subterms in
      Rewrite
        {order = order; known = known; redexes = redexes;
         subterms = subterms; waiting = waiting}
    ;;

let deleteWaiting (Rewrite r as rw) id =
    updateWaiting rw (Intset.delete r.waiting id);;

(* ------------------------------------------------------------------------- *)
(* Basic operations                                                          *)
(* ------------------------------------------------------------------------- *)

open Term_net
let newRewrite order =
    Rewrite
      {order = order;
       known = Intmap.newMap ();
       redexes = Term_net.newNet {fifo = false};
       subterms = Term_net.newNet {fifo = false};
       waiting = Intset.empty};;

let peek (Rewrite r) id = Intmap.peek r.known id;;

let size (Rewrite r) = Intmap.size r.known;;

let equations (Rewrite r) =
    Intmap.foldr (fun (_,(eqn,_),eqns) -> eqn :: eqns) [] r.known;;


(*MetisTrace1
local
  let ppEq ((x_y,_),ort) =
      Print.ppOp2 (" " ^ toStringOrientOption ort) Term.pp Term.pp x_y;;

  let ppField f ppA a =
      Print.inconsistentBlock 2
        [Print.ppString (f ^ " ="),
         Print.break,
         ppA a];;

  let ppKnown =
      ppField "known"
        (Print.ppMap Intmap.toList
           (Print.ppList (Print.ppPair Print.ppInt ppEq)));;

  let ppRedexes =
      ppField "redexes"
        (Term_net.pp (Print.ppPair Print.ppInt ppOrient));;

  let ppSubterms =
      ppField "subterms"
        (Term_net.pp
           (Print.ppMap
              (fun (i,l,p) -> (i, (if l then 0 else 1) :: p))
              (Print.ppPair Print.ppInt Term.ppPath)));;

  let ppWaiting =
      ppField "waiting"
        (Print.ppMap (Intset.toList) (Print.ppList Print.ppInt));;
in
  let pp (Rewrite r) =
      Print.inconsistentBlock 2
        [Print.ppString "Rewrite",
         Print.break,
         Print.inconsistentBlock 1
           [Print.ppString "{",
            ppKnown r.known,
(*MetisTrace5
            Print.ppString ",",
            Print.break,
            ppRedexes r.redexes,
            Print.ppString ",",
            Print.break,
            ppSubterms r.subterms,
            Print.ppString ",",
            Print.break,
            ppWaiting r.waiting,
*)
            Print.skip],
         Print.ppString "}"]
end;;
*)


(* ------------------------------------------------------------------------- *)
(* Debug functions.                                                          *)
(* ------------------------------------------------------------------------- *)

let termReducible order known id =
      let eqnRed ((l,r),_) tm =
          match total (Substitute.matchTerms Substitute.empty l) tm with
            None -> false
          | Some sub ->
            order (tm, Substitute.subst (Substitute.normalize sub) r) = Some Greater

      in let knownRed tm (eqnId,(eqn,ort)) =
          eqnId <> id &&
          ((ort <> Some Right_to_left && eqnRed eqn tm) ||
           (ort <> Some Left_to_right && eqnRed (Rule.symEqn eqn) tm))

      in let rec termRed tm = Intmap.exists (knownRed tm) known || subtermRed tm
      and subtermRed = function
          (Term.Var _) -> false
        | (Term.Fn (_,tms)) -> List.exists termRed tms
    in
      termRed
    ;;

let literalReducible order known id lit =
    List.exists (termReducible order known id) (Literal.arguments lit);;

let literalsReducible order known id lits =
    Literal.Set.exists (literalReducible order known id) lits;;

let thmReducible order known id th =
    literalsReducible order known id (Thm.clause th);;

(* ------------------------------------------------------------------------- *)
(* Add equations into the system.                                            *)
(* ------------------------------------------------------------------------- *)

let orderToOrient = function
    (Some Equal) -> raise (Error "Rewrite.orient: reflexive")
  | (Some Greater) -> Some Left_to_right
  | (Some Less) -> Some Right_to_left
  | None -> None;;

  let ins redexes redex id ort = Term_net.insert redexes (redex,(id,ort));;

  let addRedexes id (((l,r),_),ort) redexes =
      match ort with
        Some Left_to_right -> ins redexes l id Left_to_right
      | Some Right_to_left -> ins redexes r id Right_to_left
      | None -> ins (ins redexes l id Left_to_right) r id Right_to_left;;


let add (Rewrite r as rw) (id,eqn) =
  let known = r.known in
    if Intmap.inDomain id known then rw
    else
      let order = r.order in
      let redexes = r.redexes in
      let subterms = r.subterms in
      let waiting = r.waiting

        in let ort = orderToOrient (order (fst eqn))

        in let known = Intmap.insert known (id,(eqn,ort))

        in let redexes = addRedexes id (eqn,ort) redexes

        in let waiting = Intset.add waiting id

        in let rw =
            Rewrite
              {order = order; known = known; redexes = redexes;
               subterms = subterms; waiting = waiting}
(*MetisTrace5
        let () = Print.trace pp "Rewrite.add: result" rw
*)
      in
        rw
      ;;

  let uncurriedAdd (eqn,rw) = add rw eqn;;
  let addList rw = Mlist.foldl uncurriedAdd rw;;

(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order).          *)
(* ------------------------------------------------------------------------- *)

  let reorder ((i,_),(j,_)) = Int.compare (j,i);;
  let matchingRedexes redexes tm = sort reorder (Term_net.matchNet redexes tm);;


let wellOriented x y = match (x,y) with
    (None, _) -> true
  | (Some Left_to_right, Left_to_right) -> true
  | (Some Right_to_left ,Right_to_left) -> true
  | _ -> false;;

let redexResidue x y = match (x,y) with
    (Left_to_right, ((l_r,_) : equation)) -> l_r
  | (Right_to_left, ((l,r),_)) -> (r,l);;

let orientedEquation dir eqn = match dir with
    Left_to_right -> eqn
  | Right_to_left -> Rule.symEqn eqn;;

let rewrIdConv' order known redexes id tm =
      let rewr (id',lr) =
            let _ = id <> id' || raise (Error "same theorem")
            in let (eqn,ort) = Intmap.get known id'
            in let _ = wellOriented ort lr || raise (Error "orientation")
            in let (l,r) = redexResidue lr eqn
            in let sub = Substitute.normalize (Substitute.matchTerms Substitute.empty l tm)
            in let tm' = Substitute.subst sub r
            in let _ = Option.isSome ort ||
                    order (tm,tm') = Some Greater ||
                    raise (Error "order")
            in let (_,th) = orientedEquation lr eqn
          in
            (tm', Thm.subst sub th)
    in
      match first (total rewr) (matchingRedexes redexes tm) with
        None -> raise (Error "Rewrite.rewrIdConv: no matching rewrites")
      | Some res -> res
    ;;

let rewriteIdConv' order known redexes id =
    if Intmap.null known then Rule.allConv
    else Rule.repeatTopDownConv (rewrIdConv' order known redexes id);;

let mkNeqConv order lit =
      let (l,r) = Literal.destNeq lit
    in
      match order (l,r) with
        None -> raise (Error "incomparable")
      | Some Less ->
          let th = Rule.symmetryRule l r
        in
          fun tm ->
             if Term.equal tm r then (l,th) else raise (Error "mkNeqConv: RL")
      | Some Equal -> raise (Error "irreflexive")
      | Some Greater ->
          let th = Thm.assume lit
        in
          fun tm ->
             if Term.equal tm l then (r,th) else raise (Error "mkNeqConv: LR")
    ;;

type neqConvs = Neq_convs of Rule.conv Literal.Map.map;;

let neqConvsEmpty = Neq_convs (Literal.Map.newMap ());;

let neqConvsNull (Neq_convs m) = Literal.Map.null m;;

let neqConvsAdd order (Neq_convs m) lit =
    match total (mkNeqConv order) lit with
      None -> None
    | Some conv -> Some (Neq_convs (Literal.Map.insert m (lit,conv)));;

let mkNeqConvs order =
      let add (lit,(neq,lits)) =
          match neqConvsAdd order neq lit with
            Some neq -> (neq,lits)
          | None -> (neq, Literal.Set.add lits lit)
    in
      Literal.Set.foldl add (neqConvsEmpty,Literal.Set.empty)
    ;;

let neqConvsDelete (Neq_convs m) lit = Neq_convs (Literal.Map.delete m lit);;

let neqConvsToConv (Neq_convs m) =
    Rule.firstConv (Literal.Map.foldr (fun (_,c,l) -> c :: l) [] m);;

let neqConvsFoldl f b (Neq_convs m) =
    Literal.Map.foldl (fun (l,_,z) -> f (l,z)) b m;;

let neqConvsRewrIdLiterule order known redexes id neq =
    if Intmap.null known && neqConvsNull neq then Rule.allLiterule
    else
        let neq_conv = neqConvsToConv neq
        in let rewr_conv = rewrIdConv' order known redexes id
        in let conv = Rule.orelseConv neq_conv rewr_conv
        in let conv = Rule.repeatTopDownConv conv
      in
        Rule.allArgumentsLiterule conv
      ;;

let rewriteIdEqn' order known redexes id ((l_r,th) as eqn) =
      let (neq,_) = mkNeqConvs order (Thm.clause th)
      in let literule = neqConvsRewrIdLiterule order known redexes id neq
      in let (strongEqn,lit) =
          match Rule.equationLiteral eqn with
            None -> (true, Literal.mkEq l_r)
          | Some lit -> (false,lit)
      in let (lit',litTh) = literule lit
    in
      if Literal.equal lit lit' then eqn
      else
        (Literal.destEq lit',
         if strongEqn then th
         else if not (Thm.negateMember lit litTh) then litTh
         else Thm.resolve lit th litTh);;

let rewriteIdLiteralsRule' order known redexes id lits th =
      let mk_literule = neqConvsRewrIdLiterule order known redexes id

      in let rewr_neq_lit (lit, ((changed,neq,lits,th) as acc)) =
            let neq = neqConvsDelete neq lit
            in let (lit',litTh) = mk_literule neq lit
          in
            if Literal.equal lit lit' then acc
            else
                let th = Thm.resolve lit th litTh
              in
                match neqConvsAdd order neq lit' with
                  Some neq -> (true,neq,lits,th)
                | None -> (changed, neq, Literal.Set.add lits lit', th)

      in let rec rewr_neq_lits neq lits th =
            let (changed,neq,lits,th) =
                neqConvsFoldl rewr_neq_lit (false,neq,lits,th) neq
          in
            if changed then rewr_neq_lits neq lits th
            else (neq,lits,th)

      in let (neq,lits) = mkNeqConvs order lits

      in let (neq,lits,th) = rewr_neq_lits neq lits th

      in let rewr_literule = mk_literule neq

      in let rewr_lit (lit,th) =
          if Thm.member lit th then Rule.literalRule rewr_literule lit th
          else th
    in
      Literal.Set.foldl rewr_lit th lits
    ;;

let rewriteIdRule' order known redexes id th =
    rewriteIdLiteralsRule' order known redexes id (Thm.clause th) th;;

let rewrIdConv (Rewrite r) order =
    rewrIdConv' r.order r.known r.redexes;;

let rewrConv rewrite order = rewrIdConv rewrite order (-1);;

let rewriteIdConv (Rewrite r) order =
    rewriteIdConv' order r.known r.redexes;;

let rewriteConv rewrite order = rewriteIdConv rewrite order (-1);;

let rewriteIdLiteralsRule (Rewrite r) order =
    rewriteIdLiteralsRule' order r.known r.redexes;;

let rewriteLiteralsRule rewrite order =
    rewriteIdLiteralsRule rewrite order (-1);;

let rewriteIdRule (Rewrite r) order =
    rewriteIdRule' order r.known r.redexes;;

let rewriteRule rewrite order = rewriteIdRule rewrite order (-1);;

(* ------------------------------------------------------------------------- *)
(* Inter-reduce the equations in the system.                                 *)
(* ------------------------------------------------------------------------- *)

let addSubterms id (((l,r),_) : equation) subterms =
      let addSubterm b ((path,tm),net) = Term_net.insert net (tm,(id,b,path))

      in let subterms = Mlist.foldl (addSubterm true) subterms (Term.subterms l)

      in let subterms = Mlist.foldl (addSubterm false) subterms (Term.subterms r)
    in
      subterms
    ;;

let sameRedexes x y z = match (x,y,z) with
    (None,_,_) -> false
  | (Some Left_to_right, (l0,_),(l,_)) -> Term.equal l0 l
  | (Some Right_to_left, (_,r0),(_,r)) -> Term.equal r0 r;;

let redexResidues x (l,r) = match x with
    None -> [(l,r,false);(r,l,false)]
  | (Some Left_to_right) -> [(l,r,true)]
  | (Some Right_to_left) -> [(r,l,true)];;

let findReducibles order known subterms id =
      let checkValidRewr (l,r,ord) id' left path =
            let (((x,y),_),_) = Intmap.get known id'
            in let tm = Term.subterm (if left then x else y) path
            in let sub = Substitute.matchTerms Substitute.empty l tm
          in
            if ord then ()
            else
                let tm' = Substitute.subst (Substitute.normalize sub) r
              in
                if order (tm,tm') = Some Greater then ()
                else raise (Error "order")

      in let addRed lr ((id',left,path),todo) =
          if id <> id' && not (Intset.member id' todo) &&
             can (checkValidRewr lr id' left) path
          then Intset.add todo id'
          else todo

      in let findRed ((l,_,_) as lr, todo) =
          Mlist.foldl (addRed lr) todo (Term_net.matched subterms l)
    in
      Mlist.foldl findRed
    ;;

let reduce1 newx id (eqn0,ort0) (rpl,spl,todo,rw,changed) =
      let (eq0,_) = eqn0 in
      let Rewrite r = rw in
      let order = r.order in
      let known = r.known in
      let redexes = r.redexes in
      let subterms = r.subterms in
      let waiting = r.waiting
      in let (eq,_) as eqn = rewriteIdEqn' order known redexes id eqn0
      in let identical =
            let (l0,r0) = eq0
            and (l,r) = eq
          in
            Term.equal l l0 && Term.equal r r0
      in let same_redexes = identical || sameRedexes ort0 eq0 eq
      in let rpl = if same_redexes then rpl else Intset.add rpl id
      in let spl = if newx || identical then spl else Intset.add spl id
      in let changed =
          if not newx && identical then changed else Intset.add changed id
      in let ort =
          if same_redexes then Some ort0 else total orderToOrient (order eq)
    in
      match ort with
        None ->
          let known = Intmap.delete known id
          in let rw =
              Rewrite
                {order = order; known = known; redexes = redexes;
                 subterms = subterms; waiting = waiting}
        in
          (rpl,spl,todo,rw,changed)
      | Some ort ->
          let todo =
              if not newx && same_redexes then todo
              else
                findReducibles
                  order known subterms id todo (redexResidues ort eq)
          in let known =
              if identical then known else Intmap.insert known (id,(eqn,ort))
          in let redexes =
              if same_redexes then redexes
              else addRedexes id (eqn,ort) redexes
          in let subterms =
              if newx || not identical then addSubterms id eqn subterms
              else subterms
          in let rw =
              Rewrite
                {order = order; known = known; redexes = redexes;
                 subterms = subterms; waiting = waiting}
        in
          (rpl,spl,todo,rw,changed)
    ;;

let pick known set =
      let oriented id =
          match Intmap.peek known id with
            Some ((_, Some _) as x) -> Some (id,x)
          | _ -> None

      in let any id =
          match Intmap.peek known id with Some x -> Some (id,x) | _ -> None
    in
      match Intset.firstl oriented set with
        Some _ as x -> x
      | None -> Intset.firstl any set
    ;;

  let cleanRedexes known redexes rpl =
      if Intset.null rpl then redexes
      else
          let filt (id,_) = not (Intset.member id rpl)

          in let addReds (id,reds) =
              match Intmap.peek known id with
                None -> reds
              | Some eqn_ort -> addRedexes id eqn_ort reds

          in let redexes = Term_net.filter filt redexes
          in let redexes = Intset.foldl addReds redexes rpl
        in
          redexes
        ;;

  let cleanSubterms known subterms spl =
      if Intset.null spl then subterms
      else
          let filt (id,_,_) = not (Intset.member id spl)

          in let addSubtms (id,subtms) =
              match Intmap.peek known id with
                None -> subtms
              | Some (eqn,_) -> addSubterms id eqn subtms

          in let subterms = Term_net.filter filt subterms
          in let subterms = Intset.foldl addSubtms subterms spl
        in
          subterms
        ;;

  let rebuild rpl spl rw =
(*MetisTrace5
        let ppPl = Print.ppMap Intset.toList (Print.ppList Print.ppInt)
        let () = Print.trace ppPl "Rewrite.rebuild: rpl" rpl
        let () = Print.trace ppPl "Rewrite.rebuild: spl" spl
*)
        let Rewrite r = rw in
        let order = r.order in
        let known = r.known in
        let redexes = r.redexes in
        let subterms = r.subterms in
        let waiting = r.waiting
        in let redexes = cleanRedexes known redexes rpl
        in let subterms = cleanSubterms known subterms spl
      in
        Rewrite
          {order = order;
           known = known;
           redexes = redexes;
           subterms = subterms;
           waiting = waiting}
      ;;

let rec reduceAcc (rpl, spl, todo, (Rewrite r as rw), changed) =
        let known = r.known in
        let waiting = r.waiting in

    match pick known todo with
      Some (id,eqn_ort) ->
        let todo = Intset.delete todo id
      in
        reduceAcc (reduce1 false id eqn_ort (rpl,spl,todo,rw,changed))
    | None ->
      match pick known waiting with
        Some (id,eqn_ort) ->
          let rw = deleteWaiting rw id
        in
          reduceAcc (reduce1 true id eqn_ort (rpl,spl,todo,rw,changed))
      | None -> (rebuild rpl spl rw, Intset.toList changed);;

let isReduced (Rewrite r) = Intset.null r.waiting;;

let reduce' rw =
    if isReduced rw then (rw,[])
    else reduceAcc (Intset.empty,Intset.empty,Intset.empty,rw,Intset.empty);;

let reduce rw = fst (reduce' rw);;

(* ------------------------------------------------------------------------- *)
(* Rewriting as a derived rule.                                              *)
(* ------------------------------------------------------------------------- *)

  let addEqn (id_eqn,rw) = add rw id_eqn;;
  let orderedRewrite order ths =
      let rw = Mlist.foldl addEqn (newRewrite order) (enumerate ths)
    in
      rewriteRule rw order
    ;;

  let order : reductionOrder = kComb (Some Greater);;
  let rewrite = orderedRewrite order;;


end

(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS                                                 *)
(* ========================================================================= *)

module Units = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* A type of unit store.                                                     *)
(* ------------------------------------------------------------------------- *)

type unitThm = Literal.literal * Thm.thm;;

type units = Units of unitThm Literal_net.literalNet;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

open Term_net
let empty = Units (Literal_net.newNet {fifo = false});;

let size (Units net) = Literal_net.size net;;

let toString units = "U{" ^ Int.toString (size units) ^ "}";;

(* ------------------------------------------------------------------------- *)
(* Add units into the store.                                                 *)
(* ------------------------------------------------------------------------- *)

let add (Units net) ((lit,th) as uTh) =
      let net = Literal_net.insert net (lit,uTh)
    in
      match total Literal.sym lit with
        None -> Units net
      | Some ((pol,_) as lit') ->
          let th' = (if pol then Rule.symEq else Rule.symNeq) lit th
          in let net = Literal_net.insert net (lit',(lit',th'))
        in
          Units net
    ;;

let addList = Mlist.foldl (fun (th,u) -> add u th);;

(* ------------------------------------------------------------------------- *)
(* Matching.                                                                 *)
(* ------------------------------------------------------------------------- *)

let matchUnits (Units net) lit =
      let check ((lit',_) as uTh) =
          match total (Literal.matchLiterals Substitute.empty lit') lit with
            None -> None
          | Some sub -> Some (uTh,sub)
    in
      first check (Literal_net.matchNet net lit)
    ;;

(* ------------------------------------------------------------------------- *)
(* Reducing by repeated matching and resolution.                             *)
(* ------------------------------------------------------------------------- *)

let reduce units =
      let red1 (lit,news_th) =
          match total Literal.destIrrefl lit with
            Some tm ->
              let (news,th) = news_th
              in let th = Thm.resolve lit th (Thm.refl tm)
            in
              (news,th)
          | None ->
              let lit' = Literal.negate lit
            in
              match matchUnits units lit' with
                None -> news_th
              | Some ((_,rth),sub) ->
                  let (news,th) = news_th
                  in let rth = Thm.subst sub rth
                  in let th = Thm.resolve lit th rth
                  in let newLits = Literal.Set.delete (Thm.clause rth) lit'
                  in let news = Literal.Set.union newLits news
                in
                  (news,th)

      in let rec red (news,th) =
          if Literal.Set.null news then th
          else red (Literal.Set.foldl red1 (Literal.Set.empty,th) news)
    in
      fun th -> Rule.removeSym (red (Thm.clause th, th))
    ;;

end


(* ========================================================================= *)
(* CLAUSE = ID + THEOREM                                                     *)
(* ========================================================================= *)

module Clause = struct

open Useful;;
open Order;;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

let newId =
      let r = ref 0

      in let newI () =
            let n = !r

            in let () = r := n + 1
          in
            n
    in
      fun () -> Portable.critical newI ()
    ;;

(* ------------------------------------------------------------------------- *)
(* A type of clause.                                                         *)
(* ------------------------------------------------------------------------- *)

type literalOrder =
    No_literal_order
  | Unsigned_literal_order
  | Positive_literal_order;;

type parameters =
     {ordering : Knuth_bendix_order.kbo;
      orderLiterals : literalOrder;
      orderTerms : bool};;

type clauseId = int;;

type clauseInfo = {parameters : parameters; id : clauseId; thm : Thm.thm};;

type clause = Clause of clauseInfo;;


(* ------------------------------------------------------------------------- *)
(* Pretty printing.                                                          *)
(* ------------------------------------------------------------------------- *)

let toString (Clause x) = Thm.toString x.thm;;


(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let default : parameters =
    {ordering = Knuth_bendix_order.default;
     orderLiterals = Positive_literal_order;
     orderTerms = true};;

let mk info = Clause info

let dest (Clause info) = info;;

let id (Clause x) = x.id;;

let thm (Clause x) = x.thm;;

let equalThms cl cl' = Thm.equal (thm cl) (thm cl');;

let newClause parameters thm =
    Clause {parameters = parameters; id = newId (); thm = thm};;

let literals cl = Thm.clause (thm cl);;

let isTautology (Clause x) = Thm.isTautology x.thm;;

let isContradiction (Clause x) = Thm.isContradiction x.thm;;

(* ------------------------------------------------------------------------- *)
(* The term ordering is used to cut down inferences.                         *)
(* ------------------------------------------------------------------------- *)

let strictlyLess ordering x_y =
    match Knuth_bendix_order.compare ordering x_y with
      Some Less -> true
    | _ -> false;;

let isLargerTerm (p : parameters) l_r =
    not p.orderTerms || not (strictlyLess p.ordering l_r);;

  let atomToTerms atm =
      match total Atom.destEq atm with
        None -> [Term.Fn atm]
      | Some (l,r) -> [l;r];;

  let notStrictlyLess ordering (xs,ys) =
        let less x = List.exists (fun y -> strictlyLess ordering (x,y)) ys
      in
        not (Mlist.all less xs)
      ;;

  let isLargerLiteral (p : parameters) lits =
    let ordering = p.ordering in
    let orderLiterals = p.orderLiterals in
      match orderLiterals with
        No_literal_order -> kComb true
      | Unsigned_literal_order ->
          let addLit ((_,atm),acc) = atomToTerms atm @ acc

          in let tms = Literal.Set.foldl addLit [] lits
        in
          fun (_,atm') -> notStrictlyLess ordering (atomToTerms atm', tms)
      | Positive_literal_order ->
        match Literal.Set.findl (kComb true) lits with
          None -> kComb true
        | Some (pol,_) ->
            let addLit ((p,atm),acc) =
                if p = pol then atomToTerms atm @ acc else acc

            in let tms = Literal.Set.foldl addLit [] lits
          in
            fun (pol',atm') ->
               if pol <> pol' then pol
               else notStrictlyLess ordering (atomToTerms atm', tms)
          ;;


let largestLiterals (Clause x) =
    let parameters = x.parameters in
    let thm = x.thm in
      let litSet = Thm.clause thm
      in let isLarger = isLargerLiteral parameters litSet
      in let addLit (lit,s) = if isLarger lit then Literal.Set.add s lit else s
    in
      Literal.Set.foldr addLit Literal.Set.empty litSet
    ;;

(*MetisTrace6
let largestLiterals = fun cl ->
    let
      let ppResult = Literal.Set.pp
      let () = Print.trace pp "Clause.largestLiterals: cl" cl
      let result = largestLiterals cl
      let () = Print.trace ppResult "Clause.largestLiterals: result" result
    in
      result
    end;;
*)

let largestEquations (Clause x as cl) =
      let parameters = x.parameters in
      let addEq lit ort ((l,_) as l_r) acc =
          if isLargerTerm parameters l_r then (lit,ort,l) :: acc else acc

      in let addLit (lit,acc) =
          match total Literal.destEq lit with
            None -> acc
          | Some (l,r) ->
              let acc = addEq lit Rewrite.Right_to_left (r,l) acc
              in let acc = addEq lit Rewrite.Left_to_right (l,r) acc
            in
              acc
    in
      Literal.Set.foldr addLit [] (largestLiterals cl)
    ;;

  let addLit (lit,acc) =
        let addTm ((path,tm),acc) = (lit,path,tm) :: acc
      in
        Mlist.foldl addTm acc (Literal.nonVarTypedSubterms lit)
      ;;

  let largestSubterms cl = Literal.Set.foldl addLit [] (largestLiterals cl);;

  let allSubterms cl = Literal.Set.foldl addLit [] (literals cl);;

(* ------------------------------------------------------------------------- *)
(* Subsumption.                                                              *)
(* ------------------------------------------------------------------------- *)

let subsumes (subs : clause Subsume.subsume) cl =
    Subsume.isStrictlySubsumed subs (literals cl);;

(* ------------------------------------------------------------------------- *)
(* Simplifying rules: these preserve the clause id.                          *)
(* ------------------------------------------------------------------------- *)

let freshVars (Clause x) =
    Clause {parameters = x.parameters; id = x.id; thm = Rule.freshVars x.thm};;

let simplify (Clause x) =
    match Rule.simplify x.thm with
      None -> None
    | Some thm -> Some (Clause {parameters = x.parameters; id = x.id; thm = thm});;

let reduce units (Clause x) =
    Clause {parameters = x.parameters; id = x.id; thm = Units.reduce units x.thm};;

let rewrite rewr (Clause x) =
  let parameters = x.parameters in
  let id = x.id in
  let thm = x.thm in
      let simp th =
          let ordering = parameters.ordering in
          let cmp = Knuth_bendix_order.compare ordering in
            Rewrite.rewriteIdRule rewr cmp id th

(*MetisTrace4
      let () = Print.trace Rewrite.pp "Clause.rewrite: rewr" rewr
      let () = Print.trace Print.ppInt "Clause.rewrite: id" id
      let () = Print.trace pp "Clause.rewrite: cl" cl
*)

      in let thm =
          match Rewrite.peek rewr id with
            None -> simp thm
          | Some ((_,thm),_) -> if Rewrite.isReduced rewr then thm else simp thm

      in let result = Clause {parameters = parameters; id = id; thm = thm}

(*MetisTrace4
      let () = Print.trace pp "Clause.rewrite: result" result
*)
    in
      result;;

(* ------------------------------------------------------------------------- *)
(* Inference rules: these generate new clause ids.                           *)
(* ------------------------------------------------------------------------- *)

let factor (Clause x as cl) =
    let parameters = x.parameters in
    let thm = x.thm in
    let lits = largestLiterals cl in
    let apply sub = newClause parameters (Thm.subst sub thm) in
      List.map apply (Rule.factor' lits)
    ;;

(*MetisTrace5
let factor = fun cl ->
    let
      let () = Print.trace pp "Clause.factor: cl" cl
      let result = factor cl
      let () = Print.trace (Print.ppList pp) "Clause.factor: result" result
    in
      result
    end;;
*)

let resolve (cl1,lit1) (cl2,lit2) =
(*MetisTrace5
      let () = Print.trace pp "Clause.resolve: cl1" cl1
      let () = Print.trace Literal.pp "Clause.resolve: lit1" lit1
      let () = Print.trace pp "Clause.resolve: cl2" cl2
      let () = Print.trace Literal.pp "Clause.resolve: lit2" lit2
*)
      let Clause c1 = cl1 in
      let Clause c2 = cl2 in
      let parameters = c1.parameters in
      let th1 = c1.thm in
      let th2 = c2.thm in
      let sub = Literal.unify Substitute.empty lit1 (Literal.negate lit2)
(*MetisTrace5
      let () = Print.trace Substitute.pp "Clause.resolve: sub" sub
*)
      in let lit1 = Literal.subst sub lit1
      in let lit2 = Literal.negate lit1
      in let th1 = Thm.subst sub th1
      and th2 = Thm.subst sub th2
      in let _ = isLargerLiteral parameters (Thm.clause th1) lit1 ||
(*MetisTrace5
              (trace "Clause.resolve: th1 violates ordering\n";; false) ||
*)
              raise (Error "resolve: clause1: ordering constraints")
      in let _ = isLargerLiteral parameters (Thm.clause th2) lit2 ||
(*MetisTrace5
              (trace "Clause.resolve: th2 violates ordering\n";; false) ||
*)
              raise (Error "resolve: clause2: ordering constraints")
      in let th = Thm.resolve lit1 th1 th2
(*MetisTrace5
      let () = Print.trace Thm.pp "Clause.resolve: th" th
*)
      in let cl = Clause {parameters = parameters; id = newId (); thm = th}
(*MetisTrace5
      let () = Print.trace pp "Clause.resolve: cl" cl
*)
    in
      cl
    ;;

let paramodulate (cl1,lit1,ort1,tm1) (cl2,lit2,path2,tm2) =
(*MetisTrace5
      let () = Print.trace pp "Clause.paramodulate: cl1" cl1
      let () = Print.trace Literal.pp "Clause.paramodulate: lit1" lit1
      let () = Print.trace Rewrite.ppOrient "Clause.paramodulate: ort1" ort1
      let () = Print.trace Term.pp "Clause.paramodulate: tm1" tm1
      let () = Print.trace pp "Clause.paramodulate: cl2" cl2
      let () = Print.trace Literal.pp "Clause.paramodulate: lit2" lit2
      let () = Print.trace Term.ppPath "Clause.paramodulate: path2" path2
      let () = Print.trace Term.pp "Clause.paramodulate: tm2" tm2
*)
      let Clause c1 = cl1 in
      let Clause c2 = cl2 in
      let parameters = c1.parameters in
      let th1 = c1.thm in
      let th2 = c2.thm in
      let sub = Substitute.unify Substitute.empty tm1 tm2
      in let lit1 = Literal.subst sub lit1
      and lit2 = Literal.subst sub lit2
      and th1 = Thm.subst sub th1
      and th2 = Thm.subst sub th2

      in let _ = isLargerLiteral parameters (Thm.clause th1) lit1 ||
              raise (Error "Clause.paramodulate: with clause: ordering")
      in let _ = isLargerLiteral parameters (Thm.clause th2) lit2 ||
              raise (Error "Clause.paramodulate: into clause: ordering")

      in let eqn = (Literal.destEq lit1, th1)
      in let (l_r,_) as eqn =
          match ort1 with
            Rewrite.Left_to_right -> eqn
          | Rewrite.Right_to_left -> Rule.symEqn eqn
(*MetisTrace6
      let () = Print.trace Rule.ppEquation "Clause.paramodulate: eqn" eqn
*)
      in let _ = isLargerTerm parameters l_r ||
              raise (Error "Clause.paramodulate: equation: ordering constraints")
      in let th = Rule.rewrRule eqn lit2 path2 th2
(*MetisTrace5
      let () = Print.trace Thm.pp "Clause.paramodulate: th" th
*)
    in
      Clause {parameters = parameters; id = newId (); thm = th}
(*MetisTrace5
    handle Error err ->
      let
        let () = trace ("Clause.paramodulate: failed: " ^ err ^ "\n")
      in
        raise Error err
      end;;
*)


end


module Ax_cj = struct

type ax_cj_thm = {axioms_thm : Thm.thm list; conjecture_thm : Thm.thm list};;
type ax_cj_cl  = {axioms_cl : Clause.clause list; conjecture_cl : Clause.clause list};;

end

(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES                                                 *)
(* ========================================================================= *)

module Active = struct

open Useful;;
open Order;;
open Ax_cj

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* A type of active clause sets.                                             *)
(* ------------------------------------------------------------------------- *)

type simplify = {subsumes : bool; reduce : bool; rewrites : bool};;

type parameters =
     {clause : Clause.parameters;
      prefactor : simplify;
      postfactor : simplify};;

type active_t =
      {parameters : parameters;
       clauses : Clause.clause Intmap.map;
       units : Units.units;
       rewrite : Rewrite.rewrite;
       subsume : Clause.clause Subsume.subsume;
       literals : (Clause.clause * Literal.literal) Literal_net.literalNet;
       equations :
         (Clause.clause * Literal.literal * Rewrite.orient * Term.term)
         Term_net.termNet;
       subterms :
         (Clause.clause * Literal.literal * Term.path * Term.term)
         Term_net.termNet;
       allSubterms : (Clause.clause * Term.term) Term_net.termNet};;

type active =
    Active of active_t;;

let getSubsume (Active a) = a.subsume;;

let setRewrite active rewrite =
    let Active a = active in
    let parameters = a.parameters in
    let clauses = a.clauses in
    let units = a.units in
    let subsume = a.subsume in
    let literals = a.literals in
    let equations = a.equations in
    let subterms = a.subterms in
    let allSubterms = a.allSubterms in
      Active
        {parameters = parameters; clauses = clauses; units = units;
         rewrite = rewrite; subsume = subsume; literals = literals;
         equations = equations; subterms = subterms; allSubterms = allSubterms}
    ;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let maxSimplify : simplify = {subsumes = true; reduce = true; rewrites = true};;

let default : parameters =
    {clause = Clause.default;
     prefactor = maxSimplify;
     postfactor = maxSimplify};;

open Term_net
let empty parameters =
    let clause = parameters.clause in
    let ordering = clause.Clause.ordering in
      Active
        {parameters = parameters;
         clauses = Intmap.newMap ();
         units = Units.empty;
         rewrite = Rewrite.newRewrite (Knuth_bendix_order.compare ordering);
         subsume = Subsume.newSubsume ();
         literals = Literal_net.newNet {fifo = false};
         equations = Term_net.newNet {fifo = false};
         subterms = Term_net.newNet {fifo = false};
         allSubterms = Term_net.newNet {fifo = false}}
    ;;

let size (Active a) = Intmap.size a.clauses;;

let clauses (Active a) =
      let add (_,cl,acc) = cl :: acc
    in
      Intmap.foldr add [] a.clauses
    ;;

let saturation active =
      let remove (cl,(cls,subs)) =
            let lits = Clause.literals cl
          in
            if Subsume.isStrictlySubsumed subs lits then (cls,subs)
            else (cl :: cls, Subsume.insert subs (lits,()))

      in let cls = clauses active
      in let (cls,_) = Mlist.foldl remove ([], Subsume.newSubsume ()) cls
      in let (cls,subs) = Mlist.foldl remove ([], Subsume.newSubsume ()) cls

    in
      cls
    ;;


(* ------------------------------------------------------------------------- *)
(* Pretty printing.                                                          *)
(* ------------------------------------------------------------------------- *)

let toString active = "Active{" ^ string_of_int (size active) ^ "}";;


(* ------------------------------------------------------------------------- *)
(* Simplify clauses.                                                         *)
(* ------------------------------------------------------------------------- *)

let simplify simp units rewr subs =
    let s = simp.subsumes in
    let r = simp.reduce in
    let w = simp.rewrites in
    let rewrite cl =
            let cl' = Clause.rewrite rewr cl
          in
            if Clause.equalThms cl cl' then Some cl else Clause.simplify cl'
    in
      fun cl ->
         match Clause.simplify cl with
           None -> None
         | Some cl ->
           match (if w then rewrite cl else Some cl) with
             None -> None
           | Some cl ->
               let cl = if r then Clause.reduce units cl else cl
             in
               if s && Clause.subsumes subs cl then None else Some cl
    ;;

let simplifyActive simp active =
    let Active a = active in
      simplify simp a.units a.rewrite a.subsume
    ;;

(* ------------------------------------------------------------------------- *)
(* Add a clause into the active set.                                         *)
(* ------------------------------------------------------------------------- *)

let addUnit units cl =
      let th = Clause.thm cl
    in
      match total Thm.destUnit th with
        Some lit -> Units.add units (lit,th)
      | None -> units
    ;;

let addRewrite rewrite cl =
      let th = Clause.thm cl
    in
      match total Thm.destUnitEq th with
        Some l_r -> Rewrite.add rewrite (Clause.id cl, (l_r,th))
      | None -> rewrite
    ;;

let addSubsume subsume cl = Subsume.insert subsume (Clause.literals cl, cl);;

let addLiterals literals cl =
      let add ((_,atm) as lit, literals) =
          if Atom.isEq atm then literals
          else Literal_net.insert literals (lit,(cl,lit))
    in
      Literal.Set.foldl add literals (Clause.largestLiterals cl)
    ;;

let addEquations equations cl =
      let add ((lit,ort,tm),equations) =
          Term_net.insert equations (tm,(cl,lit,ort,tm))
    in
      Mlist.foldl add equations (Clause.largestEquations cl)
    ;;

let addSubterms subterms cl =
      let add ((lit,path,tm),subterms) =
          Term_net.insert subterms (tm,(cl,lit,path,tm))
    in
      Mlist.foldl add subterms (Clause.largestSubterms cl)
    ;;

let addAllSubterms allSubterms cl =
      let add ((_,_,tm),allSubterms) =
          Term_net.insert allSubterms (tm,(cl,tm))
    in
      Mlist.foldl add allSubterms (Clause.allSubterms cl)
    ;;

let addClause active cl =
    let Active a = active in
    let parameters = a.parameters in
    let clauses = a.clauses in
    let units = a.units in
    let rewrite = a.rewrite in
    let subsume = a.subsume in
    let literals = a.literals in
    let equations = a.equations in
    let subterms = a.subterms in
    let allSubterms = a.allSubterms in
      let clauses = Intmap.insert clauses (Clause.id cl, cl)
      and subsume = addSubsume subsume cl
      and literals = addLiterals literals cl
      and equations = addEquations equations cl
      and subterms = addSubterms subterms cl
      and allSubterms = addAllSubterms allSubterms cl
    in
      Active
        {parameters = parameters; clauses = clauses; units = units;
         rewrite = rewrite; subsume = subsume; literals = literals;
         equations = equations; subterms = subterms;
         allSubterms = allSubterms}
    ;;

let addFactorClause active cl =
    let Active a = active in
    let parameters = a.parameters in
    let clauses = a.clauses in
    let units = a.units in
    let rewrite = a.rewrite in
    let subsume = a.subsume in
    let literals = a.literals in
    let equations = a.equations in
    let subterms = a.subterms in
    let allSubterms = a.allSubterms in
      let units = addUnit units cl
      and rewrite = addRewrite rewrite cl
    in
      Active
        {parameters = parameters; clauses = clauses; units = units;
         rewrite = rewrite; subsume = subsume; literals = literals;
         equations = equations; subterms = subterms; allSubterms = allSubterms}
    ;;

(* ------------------------------------------------------------------------- *)
(* Derive (unfactored) consequences of a clause.                             *)
(* ------------------------------------------------------------------------- *)

let deduceResolution literals cl ((_,atm) as lit, acc) =
      let resolve (cl_lit,acc) =
          (*let (cl1, lit1) = cl_lit in
          print_endline ("cl1 = " ^ Clause.toString cl1);
          print_endline ("lit1 = " ^ Literal.toString lit1);
          print_endline ("cl = " ^ Clause.toString cl);
          print_endline ("lit = " ^ Literal.toString lit);*)
          match total (Clause.resolve cl_lit) (cl,lit) with
            Some cl' -> cl' :: acc
          | None -> acc
(*MetisTrace4
      let () = Print.trace Literal.pp "Active.deduceResolution: lit" lit
*)
    in
      if Atom.isEq atm then acc
      else
        Mlist.foldl resolve acc (Literal_net.unify literals (Literal.negate lit))
    ;;

let deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =
      let para (cl_lit_path_tm,acc) =
          match total (Clause.paramodulate (cl,lit,ort,tm)) cl_lit_path_tm with
            Some cl' -> cl' :: acc
          | None -> acc
    in
      Mlist.foldl para acc (Term_net.unify subterms tm)
    ;;

let deduceParamodulationInto equations cl ((lit,path,tm),acc) =
      let para (cl_lit_ort_tm,acc) =
          match total (Clause.paramodulate cl_lit_ort_tm) (cl,lit,path,tm) with
            Some cl' -> cl' :: acc
          | None -> acc
    in
      Mlist.foldl para acc (Term_net.unify equations tm)
    ;;

let deduce active cl =
    let Active a = active in
    let parameters = a.parameters in
    let literals = a.literals in
    let equations = a.equations in
    let subterms = a.subterms in
      let lits = Clause.largestLiterals cl
      in let eqns = Clause.largestEquations cl
      in let subtms =
          if Term_net.null equations then [] else Clause.largestSubterms cl
(*MetisTrace5
      let () = Print.trace Literal.Set.pp "Active.deduce: lits" lits
      let () = Print.trace
                 (Print.ppList
                    (Print.ppMap (fun (lit,ort,_) -> (lit,ort))
                      (Print.ppPair Literal.pp Rewrite.ppOrient)))
                 "Active.deduce: eqns" eqns
      let () = Print.trace
                 (Print.ppList
                    (Print.ppTriple Literal.pp Term.ppPath Term.pp))
                 "Active.deduce: subtms" subtms
*)

      in let acc = []
      in let acc = Literal.Set.foldl (deduceResolution literals cl) acc lits
      in let acc = Mlist.foldl (deduceParamodulationWith subterms cl) acc eqns
      in let acc = Mlist.foldl (deduceParamodulationInto equations cl) acc subtms
      in let acc = List.rev acc

(*MetisTrace5
      let () = Print.trace (Print.ppList Clause.pp) "Active.deduce: acc" acc
*)
    in
      acc
    ;;

(* ------------------------------------------------------------------------- *)
(* Extract clauses from the active set that can be simplified.               *)
(* ------------------------------------------------------------------------- *)

  let clause_rewritables active =
    let Active a = active in
    let clauses = a.clauses in
    let rewrite = a.rewrite in
        let rewr (id,cl,ids) =
              let cl' = Clause.rewrite rewrite cl
            in
              if Clause.equalThms cl cl' then ids else Intset.add ids id
      in
        Intmap.foldr rewr Intset.empty clauses
      ;;

  let orderedRedexResidues (((l,r),_),ort) =
      match ort with
        None -> []
      | Some Rewrite.Left_to_right -> [(l,r,true)]
      | Some Rewrite.Right_to_left -> [(r,l,true)];;

  let unorderedRedexResidues (((l,r),_),ort) =
      match ort with
        None -> [(l,r,false);(r,l,false)]
      | Some _ -> [];;

  let rewrite_rewritables active rewr_ids =
    let Active a = active in
    let parameters = a.parameters in
    let clauses = a.clauses in
    let rewrite = a.rewrite in
    let allSubterms = a.allSubterms in
        let ordering = parameters.clause.Clause.ordering
        in let order = Knuth_bendix_order.compare ordering

        in let addRewr (id,acc) =
            if Intmap.inDomain id clauses then Intset.add acc id else acc

        in let addReduce ((l,r,ord),acc) =
              let isValidRewr tm =
                  match total (Substitute.matchTerms Substitute.empty l) tm with
                    None -> false
                  | Some sub ->
                    ord ||
                      let tm' = Substitute.subst (Substitute.normalize sub) r
                    in
                      order (tm,tm') = Some Greater

              in let addRed ((cl,tm),acc) =
(*MetisTrace5
                    let () = Print.trace Clause.pp "Active.addRed: cl" cl
                    let () = Print.trace Term.pp "Active.addRed: tm" tm
*)
                    let id = Clause.id cl
                  in
                    if Intset.member id acc then acc
                    else if not (isValidRewr tm) then acc
                    else Intset.add acc id

(*MetisTrace5
              let () = Print.trace Term.pp "Active.addReduce: l" l
              let () = Print.trace Term.pp "Active.addReduce: r" r
              let () = Print.trace Print.ppBool "Active.addReduce: ord" ord
*)
            in
              Mlist.foldl addRed acc (Term_net.matched allSubterms l)

        in let addEquation redexResidues (id,acc) =
            match Rewrite.peek rewrite id with
              None -> acc
            | Some eqn_ort -> Mlist.foldl addReduce acc (redexResidues eqn_ort)

        in let addOrdered = addEquation orderedRedexResidues

        in let addUnordered = addEquation unorderedRedexResidues

        in let ids = Intset.empty
        in let ids = Mlist.foldl addRewr ids rewr_ids
        in let ids = Mlist.foldl addOrdered ids rewr_ids
        in let ids = Mlist.foldl addUnordered ids rewr_ids
      in
        ids
      ;;

  let choose_clause_rewritables active ids = size active <= length ids

  let rewritables active ids =
      if choose_clause_rewritables active ids then clause_rewritables active
      else rewrite_rewritables active ids;;

  let delete active ids =
      if Intset.null ids then active
      else
          let idPred id = not (Intset.member id ids) in
          let clausePred cl = idPred (Clause.id cl) in

          let Active a = active in
          let parameters = a.parameters in
          let clauses = a.clauses in
          let units = a.units in
          let subsume = a.subsume in
          let rewrite = a.rewrite in
          let literals = a.literals in
          let equations = a.equations in
          let subterms = a.subterms in
          let allSubterms = a.allSubterms in

          let cP1 (x,_) = clausePred x
          in let cP1_4 (x,_,_,_) = clausePred x
          in let clauses = Intmap.filter (fun x -> idPred (fst x)) clauses
          and subsume = Subsume.filter clausePred subsume
          and literals = Literal_net.filter cP1 literals
          and equations = Term_net.filter cP1_4 equations
          and subterms = Term_net.filter cP1_4 subterms
          and allSubterms = Term_net.filter cP1 allSubterms
        in
          Active
            {parameters = parameters;
             clauses = clauses;
             units = units;
             rewrite = rewrite;
             subsume = subsume;
             literals = literals;
             equations = equations;
             subterms = subterms;
             allSubterms = allSubterms}
        ;;

  let extract_rewritables (Active a as active) =
    let clauses = a.clauses in
    let rewrite = a.rewrite in
      if Rewrite.isReduced rewrite then (active,[])
      else
(*MetisTrace3
          let () = trace "Active.extract_rewritables: inter-reducing\n"
*)
          let (rewrite,ids) = Rewrite.reduce' rewrite
          in let active = setRewrite active rewrite
          in let ids = rewritables active ids
          in let cls = Intset.transform (Intmap.get clauses) ids
(*MetisTrace3
          let ppCls = Print.ppList Clause.pp
          let () = Print.trace ppCls "Active.extract_rewritables: cls" cls
*)
        in
          (delete active ids, cls)
;;

(* ------------------------------------------------------------------------- *)
(* Factor clauses.                                                           *)
(* ------------------------------------------------------------------------- *)

  let prefactor_simplify active subsume =
    let Active a = active in
    let parameters = a.parameters in
    let units = a.units in
    let rewrite = a.rewrite in
    let prefactor = parameters.prefactor in
      simplify prefactor units rewrite subsume
      ;;

  let postfactor_simplify active subsume =
    let Active a = active in
    let parameters = a.parameters in
    let units = a.units in
    let rewrite = a.rewrite in
    let postfactor = parameters.postfactor in
      simplify postfactor units rewrite subsume
      ;;

  let sort_utilitywise =
        let utility cl =
            match Literal.Set.size (Clause.literals cl) with
              0 -> -1
            | 1 -> if Thm.isUnitEq (Clause.thm cl) then 0 else 1
            | n -> n
      in
        sortMap utility Int.compare
      ;;

  let rec post_factor (cl, ((active,subsume,acc) as active_subsume_acc)) =
      match postfactor_simplify active subsume cl with
        None -> active_subsume_acc
      | Some cl' ->
          if Clause.equalThms cl' cl then
            let active = addFactorClause active cl
            and subsume = addSubsume subsume cl
            and acc = cl :: acc
            in (active,subsume,acc)
          else
            (* If the clause was changed in the post-factor simplification *)
            (* step, then it may have altered the set of largest literals *)
            (* in the clause. The safest thing to do is to factor again. *)
            factor1 (cl', active_subsume_acc)

  and factor1 (cl, active_subsume_acc) =
      let cls = sort_utilitywise (cl :: Clause.factor cl)
      in Mlist.foldl post_factor active_subsume_acc cls
      ;;

  let pre_factor (cl, ((active,subsume,_) as active_subsume_acc)) =
      match prefactor_simplify active subsume cl with
        None -> active_subsume_acc
      | Some cl -> factor1 (cl, active_subsume_acc)
      ;;

  let rec factor' active acc = function
      [] -> (active, List.rev acc)
    | cls ->
        let cls = sort_utilitywise cls
        in let subsume = getSubsume active
        in let (active,_,acc) = Mlist.foldl pre_factor (active,subsume,acc) cls
        in let (active,cls) = extract_rewritables active
      in
        factor' active acc cls
      ;;

  let factor active cls = factor' active [] cls;;

(*let factor active cls =
  let str cl = String.concat "\n" (List.map Clause.toString cl) in
  print_endline ("Active.factor: cls:\n" ^ str cls);
  let (active,cls') = factor active cls in
  print_endline ("Active.factor: cls':\n" ^ str cls');
  (active, cls');;
*)

(*MetisTrace4
let factor = fun active -> fun cls ->
    let
      let ppCls = Print.ppList Clause.pp
      let () = Print.trace ppCls "Active.factor: cls" cls
      let (active,cls') = factor active cls
      let () = Print.trace ppCls "Active.factor: cls'" cls'
    in
      (active,cls')
    end;;
*)

(* ------------------------------------------------------------------------- *)
(* Create a new active clause set and initialize clauses.                    *)
(* ------------------------------------------------------------------------- *)

let mk_clause params th =
  Clause.mk {Clause.parameters = params; Clause.id = Clause.newId (); Clause.thm = th};;

let newActive parameters x =
      let axioms_thm = x.axioms_thm in
      let conjecture_thm = x.conjecture_thm in
      let clause = parameters.clause
      in let mk_clause = mk_clause clause
      in let active = empty parameters
      in let (active,axioms) = factor active (List.map mk_clause axioms_thm)
      in let (active,conjecture) = factor active (List.map mk_clause conjecture_thm)
    in
      (active, {axioms_cl = axioms; conjecture_cl = conjecture})
    ;;

(* ------------------------------------------------------------------------- *)
(* Add a clause into the active set and deduce all consequences.             *)
(* ------------------------------------------------------------------------- *)

let add active cl =
    match simplifyActive maxSimplify active cl with
      None -> (active,[])
    | Some cl' ->
      if Clause.isContradiction cl' then (active,[cl'])
      else if not (Clause.equalThms cl cl') then factor active [cl']
      else
(*MetisTrace2
          let () = Print.trace Clause.pp "Active.add: cl" cl
*)
          let active = addClause active cl
          in let cl = Clause.freshVars cl
          in let cls = deduce active cl
          in let (active,cls) = factor active cls
(*MetisTrace2
          let ppCls = Print.ppList Clause.pp
          let () = Print.trace ppCls "Active.add: cls" cls
*)
        in
          (active,cls)
        ;;

end


(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES                                                *)
(* ========================================================================= *)

module Waiting = struct

open Useful;;
open Ax_cj
open Real

(* ------------------------------------------------------------------------- *)
(* A type of waiting sets of clauses.                                        *)
(* ------------------------------------------------------------------------- *)

type weight = real;;

type modelParameters =
     {model : Model.parameters;
      initialPerturbations : int;
      maxChecks : int option;
      perturbations : int;
      weight : weight}

type parameters =
     {symbolsWeight : weight;
      variablesWeight : weight;
      literalsWeight : weight;
      modelsP : modelParameters list};;

type distance = real;;

type waiting_t =
      {parameters : parameters;
       clauses : (weight * (distance * Clause.clause)) Heap.heap;
       models : Model.model list};;

type waiting =
    Waiting of waiting_t;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let defaultModels : modelParameters list =
    [{model = Model.default;
      initialPerturbations = 100;
      maxChecks = Some 20;
      perturbations = 0;
      weight = 1.0}];;

let default : parameters =
     {symbolsWeight = 1.0;
      literalsWeight = 1.0;
      variablesWeight = 1.0;
      modelsP = defaultModels};;

let size (Waiting w) = Heap.size w.clauses;;

let toString w = "Waiting{" ^ Int.toString (size w) ^ "}";;

(*let toString (Waiting w) = "\n" ^
  String.concat "\n" (List.map (fun (w, (d, c)) -> Clause.toString c) (Heap.toList w.clauses));;*)


(* ------------------------------------------------------------------------- *)
(* Perturbing the models.                                                    *)
(* ------------------------------------------------------------------------- *)

type modelClause = Name.Set.set * Thm.clause;;

let mkModelClause cl =
      let lits = Clause.literals cl
      in let fvs = Literal.Set.freeVars lits
    in
      (fvs,lits)
    ;;

let mkModelClauses = List.map mkModelClause;;

let perturbModel vM cls =
    if Mlist.null cls then kComb ()
    else
        let vN = {Model.size = Model.msize vM}

        in let perturbClause (fv,cl) =
              let vV = Model.randomValuation vN fv
            in
              if Model.interpretClause vM vV cl then ()
              else Model.perturbClause vM vV cl

        in let perturbClauses () = app perturbClause cls
      in
        fun n -> funpow n perturbClauses ()
      ;;

let initialModel axioms conjecture parm =
      let model = parm.model in
      let initialPerturbations = parm.initialPerturbations in
      let m = Model.newModel model
      in let () = perturbModel m conjecture initialPerturbations
      in let () = perturbModel m axioms initialPerturbations
    in
      m
    ;;

let checkModels parms models (fv,cl) =
      let check ((parm,model),z) =
          let maxChecks = parm.maxChecks in
          let weight = parm.weight in
          let n = maxChecks in
          let (vT,vF) = Model.check Model.interpretClause n model fv cl in
            Math.pow (1.0 +. Real.fromInt vT /. Real.fromInt (vT + vF), weight) *. z
    in
      Mlist.foldl check 1.0 (zip parms models)
    ;;

let perturbModels parms models cls =
      let perturb (parm,model) =
          let perturbations = parm.perturbations in
            perturbModel model cls perturbations
    in
      app perturb (zip parms models)
    ;;

(* ------------------------------------------------------------------------- *)
(* Clause weights.                                                           *)
(* ------------------------------------------------------------------------- *)

  let clauseSymbols cl = Real.fromInt (Literal.Set.typedSymbols cl);;

  let clauseVariables cl =
      Real.fromInt (Name.Set.size (Literal.Set.freeVars cl) + 1);;

  let clauseLiterals cl = Real.fromInt (Literal.Set.size cl);;

  let clausePriority cl = 1e-12 *. Real.fromInt (Clause.id cl);;

  let clauseWeight (parm : parameters) mods dist mcl cl =
(*MetisTrace3
        let () = Print.trace Clause.pp "Waiting.clauseWeight: cl" cl
*)
        let symbolsWeight = parm.symbolsWeight in
        let variablesWeight = parm.variablesWeight in
        let literalsWeight = parm.literalsWeight in
        let modelsP = parm.modelsP in
        let lits = Clause.literals cl
        in let symbolsW = Math.pow (clauseSymbols lits, symbolsWeight)
        in let variablesW = Math.pow (clauseVariables lits, variablesWeight)
        in let literalsW = Math.pow (clauseLiterals lits, literalsWeight)
        in let modelsW = checkModels modelsP mods mcl
(*MetisTrace4
        let () = trace ("Waiting.clauseWeight: dist = " ^
                        Real.toString dist ^ "\n")
        let () = trace ("Waiting.clauseWeight: symbolsW = " ^
                        Real.toString symbolsW ^ "\n")
        let () = trace ("Waiting.clauseWeight: variablesW = " ^
                        Real.toString variablesW ^ "\n")
        let () = trace ("Waiting.clauseWeight: literalsW = " ^
                        Real.toString literalsW ^ "\n")
        let () = trace ("Waiting.clauseWeight: modelsW = " ^
                        Real.toString modelsW ^ "\n")
*)
        in let weight = dist *. symbolsW *. variablesW *. literalsW *. modelsW
        in let weight = weight +. clausePriority cl
(*MetisTrace3
        let () = trace ("Waiting.clauseWeight: weight = " ^
                        Real.toString weight ^ "\n")
*)
      in
        weight
      ;;

(* ------------------------------------------------------------------------- *)
(* Adding new clauses.                                                       *)
(* ------------------------------------------------------------------------- *)

let add' waiting dist mcls cls =
      let Waiting w = waiting in
      let parameters = w.parameters in
      let clauses = w.clauses in
      let models = w.models in
      let modelParameters = parameters.modelsP

      in let dist = dist +. Math.ln (Real.fromInt (length cls))

      in let addCl ((mcl,cl),acc) =
            let weight = clauseWeight parameters models dist mcl cl
          in
            Heap.add acc (weight,(dist,cl))

      in let clauses = Mlist.foldl addCl clauses (zip mcls cls)

      in let () = perturbModels modelParameters models mcls
    in
      Waiting {parameters = parameters; clauses = clauses; models = models}
    ;;

let add waiting (dist,cls) =
    if Mlist.null cls then waiting
    else
(*MetisTrace3
        let () = Print.trace pp "Waiting.add: waiting" waiting
        let () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
*)

        let waiting = add' waiting dist (mkModelClauses cls) cls

(*MetisTrace3
        let () = Print.trace pp "Waiting.add: waiting" waiting
*)
      in
        waiting
      ;;

  let cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);;

  let empty parameters axioms conjecture =
        let modelParameters = parameters.modelsP
        in let clauses = Heap.newHeap cmp
        and models = List.map (initialModel axioms conjecture) modelParameters
      in
        Waiting {parameters = parameters; clauses = clauses; models = models}
      ;;

  let newWaiting parameters x =
      let axioms_cl = x.axioms_cl in
      let conjecture_cl = x.conjecture_cl in
        let mAxioms = mkModelClauses axioms_cl
        and mConjecture = mkModelClauses conjecture_cl

        in let waiting = empty parameters mAxioms mConjecture
      in
        if Mlist.null axioms_cl && Mlist.null conjecture_cl then waiting
        else add' waiting 0.0 (mAxioms @ mConjecture) (axioms_cl @ conjecture_cl)
      ;;

(* ------------------------------------------------------------------------- *)
(* Removing the lightest clause.                                             *)
(* ------------------------------------------------------------------------- *)

let remove (Waiting w) =
  let parameters = w.parameters in
  let clauses = w.clauses in
  let models = w.models in
    if Heap.null clauses then None
    else
        let ((_,dcl),clauses) = Heap.remove clauses

        in let waiting =
            Waiting
              {parameters = parameters;
               clauses = clauses;
               models = models}
      in
        Some (dcl,waiting)
      ;;

end


(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE                                            *)
(* ========================================================================= *)

module Resolution = struct

open Useful;;

(* ------------------------------------------------------------------------- *)
(* A type of resolution proof procedures.                                    *)
(* ------------------------------------------------------------------------- *)

type parameters =
     {activeP : Active.parameters;
      waitingP : Waiting.parameters};;

type resolution_t =
      {parameters : parameters;
       active : Active.active;
       waiting : Waiting.waiting};;

type resolution =
    Resolution of resolution_t;;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

let default : parameters =
    {activeP = Active.default;
     waitingP = Waiting.default};;

let newResolution parameters ths =
      let activeParm = parameters.activeP in
      let waitingParm = parameters.waitingP in
      let (active,cls) = Active.newActive activeParm ths  (* cls = factored ths *)

      in let waiting = Waiting.newWaiting waitingParm cls
    in
      Resolution {parameters = parameters; active = active; waiting = waiting};;

let active (Resolution r) = r.active;;

let waiting (Resolution r) = r.waiting;;


(* ------------------------------------------------------------------------- *)
(* The main proof loop.                                                      *)
(* ------------------------------------------------------------------------- *)

type decision =
    Contradiction of Thm.thm
  | Satisfiable of Thm.thm list;;

type state =
    Decided of decision
  | Undecided of resolution;;

let iterate res =
      let Resolution r = res in
      let parameters = r.parameters in
      let active = r.active in
      let waiting = r.waiting in

(*MetisTrace2
      let () = Print.trace Active.pp "Resolution.iterate: active" active
      let () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting
*)
      (*
      print_endline ("Resolution.iterate:active: " ^ Active.toString active);
      print_endline ("Resolution.iterate:waiting: " ^ Waiting.toString waiting);
      *)
      match Waiting.remove waiting with
        None ->
          let sat = Satisfiable (List.map Clause.thm (Active.saturation active))
        in
          Decided sat
      | Some ((d,cl),waiting) ->
        if Clause.isContradiction cl then
          Decided (Contradiction (Clause.thm cl))
        else
(*MetisTrace1
            let () = Print.trace Clause.pp "Resolution.iterate: cl" cl
*)
            (*
            let () = print_endline ("Resolution.iterate: cl " ^ (Clause.toString cl)) in
            *)
            let (active,cls) = Active.add active cl

            in let waiting = Waiting.add waiting (d,cls)

            in let res =
                Resolution
                  {parameters = parameters;
                   active = active;
                   waiting = waiting}
          in
            Undecided res
    ;;

let rec loop res =
    match iterate res with
      Decided dec -> dec
    | Undecided res -> loop res;;


end

(* ========================================================================= *)
(* The basic Metis loop.                                                     *)
(* ========================================================================= *)

module Loop =
struct

let rec loop res =
  match Resolution.iterate res with
    Resolution.Decided dec -> Some dec
  | Resolution.Undecided res -> loop res

open Ax_cj

let run rules =
  let ths = {axioms_thm = rules; conjecture_thm = []} in
  let res = Resolution.newResolution Resolution.default ths in
  match loop res with
    None -> failwith "metis: timeout"
  | Some (Resolution.Contradiction thm) -> thm
  | Some (Resolution.Satisfiable _) ->
      failwith "metis: found satisfiable assignment"

end

end


module Metis_debug = struct

(* Taken from: https://sourceforge.net/p/hol/mailman/message/35201767/ *)
let print_varandtype fmt tm =
   let hop,args = strip_comb tm in
   let s = name_of hop
   and ty = type_of hop in
   if is_var hop && args = [] then
    (pp_print_string fmt "(";
     pp_print_string fmt s;
     pp_print_string fmt ":";
     pp_print_type fmt ty;
     pp_print_string fmt ")")
   else fail() ;;

let show_types,hide_types =
   (fun () -> install_user_printer ("Show Types",print_varandtype)),
   (fun () -> try delete_user_printer "Show Types"
              with Failure _ -> failwith ("hide_types: "^
                                          "Types are already hidden."));;

end


module Preterm = struct

let mk_negp pt = Combp (preterm_of_term `~`, pt)
let mk_eqp (ps, pt) = Combp (Combp (Constp ("=", dpty), ps), pt)
let mk_conjp (ps, pt) = Combp (Combp (preterm_of_term `/\`, ps), pt)
let mk_disjp (ps, pt) = Combp (Combp (preterm_of_term `\/`, ps), pt)

let list_mk_combp (h, t) = rev_itlist (fun x acc -> Combp (acc, x)) t h

assert
  (
    list_mk_combp (Varp ("1", dpty), [Varp ("2", dpty); Varp ("3", dpty)])
  =
    Combp (Combp (Varp ("1", Ptycon ("", [])), Varp ("2", Ptycon ("", []))),
      Varp ("3", Ptycon ("", [])))
  );;

let list_mk_disjp = function
    [] -> preterm_of_term `F`
  | h::t -> itlist (curry mk_disjp) t h

(* typechecking a preterm with constants fails,
   therefore we convert constants to variables before type checking
   type checking converts the variables back to the corresponding constants
*)
let rec unconst_preterm = function
    Varp (s, pty) -> Varp (s, pty)
  | Constp (s, pty) -> Varp (s, pty)
  | Combp (l, r) -> Combp (unconst_preterm l, unconst_preterm r)
  | Typing (ptm, pty) -> Typing (unconst_preterm ptm, pty)
  | _ -> failwith "unconst_preterm"

let rec env_of_preterm = function
    Varp (s, pty) -> [(s, pty)]
  | Constp (s, pty) -> []
  | Combp (l, r) -> env_of_preterm l @ env_of_preterm r
  | Typing (ptm, pty) -> env_of_preterm ptm
  | _ -> failwith "env_of_preterm"

let env_of_th = env_of_preterm o preterm_of_term o concl
let env_of_ths = List.concat o List.map env_of_th

end


module Metis_mapping = struct

open Metis_prover

  let reset_consts,fol_of_const,hol_of_const =
    Meson.reset_consts,Meson.fol_of_const,Meson.hol_of_const

let preterm_of_const = preterm_of_term o hol_of_const o int_of_string

let prefix s = "__" ^ s

let rec preterm_of_fol_term = function
    Term.Var x -> Varp (prefix x, dpty)
  | Term.Fn (f, args) ->
      let pf = preterm_of_const f in
      let pargs = List.map preterm_of_fol_term args in
      Preterm.list_mk_combp (pf, pargs)

let preterm_of_predicate = function
    "=" -> Constp ("=", dpty)
  | p -> preterm_of_const p

let preterm_of_atom (p, args) =
  let pp = preterm_of_predicate p in
  let pargs = List.map preterm_of_fol_term args in
  Typing (Preterm.list_mk_combp (pp, pargs), pretype_of_type bool_ty)

let preterm_of_literal (pol, fat) =
  let pat = preterm_of_atom fat in
  if pol then pat else Preterm.mk_negp pat

let preterm_of_eq (s, t) =
  Preterm.mk_eqp (preterm_of_fol_term s, preterm_of_fol_term t)


let typecheck env = term_of_preterm o retypecheck env o Preterm.unconst_preterm
let typecheckl env = function
    [] -> []
  | xs -> Preterm.list_mk_disjp xs |> typecheck env |> disjuncts


let hol_of_term env = typecheck env o preterm_of_fol_term

let hol_of_atom env = typecheck env o preterm_of_atom

let hol_of_literal env = typecheck env o preterm_of_literal

let hol_of_clause env = typecheck env o Preterm.list_mk_disjp o map preterm_of_literal

let hol_of_substitution env = map dest_eq o typecheckl env o map preterm_of_eq

end


module Metis_path = struct

open Metis_prover

(* The term `f 1 2 3` is encoded in HOL Light as follows:

         @
        / \
       @  3
      / \
     @  2
    / \
   f  1

*)

let rec hol_of_term_path tm path = match tm, path with
    (tm, []) -> tm, ""
  | Term.Fn (f, args), i :: is ->
      let arity = length args in
      assert (i < arity);
      let (tm', path') = hol_of_term_path (List.nth args i) is in
      (tm', String.make (arity - i - 1) 'l' ^ "r" ^ path')
  | _ -> failwith "hol_of_term_path"

let hol_of_atom_path (p, args) = hol_of_term_path (Term.Fn (p, args))

let hol_of_literal_path (pol, atom) path =
  let s, path = hol_of_atom_path atom path in
  s, if pol then path else "r" ^ path

end


module Metis_unify = struct

open Metis_prover

let verb = ref false

exception Unify

let rec unify_fo_ho_term vars fat tm m =
  if !verb then Format.printf "unify_fo_ho_term: fat = %s, tm = %s\n%!"
    (Term.toString fat) (string_of_term tm);
  match fat with
    Term.Var v when List.mem_assoc v m ->
      if !verb then Format.printf "var_assoc\n%!";
      let tm' = List.assoc v m in
      if tm = tm' then m else raise Unify
  | Term.Var v ->
      if !verb then Format.printf "var\n%!";
      if is_var tm && not (List.mem tm vars) then (v, tm) :: m
      else (if !verb then Format.printf "Unify!\n%!"; raise Unify)
  | Term.Fn (f, args) ->
      if !verb then Format.printf "fn\n%!";
      let hf, hargs = try strip_comb tm with _ -> raise Unify in
      if !verb then begin
        Format.printf "hf = %s\n%!" (string_of_term hf);
        Format.printf "is_var: %s\n%!" (if is_var hf then "true" else "false")
      end;
      assert (is_const hf || is_var hf);
      if hf = Metis_mapping.hol_of_const (int_of_string f)
      then itlist2 (unify_fo_ho_term vars) args hargs m
      else raise Unify

let unify_fo_ho_atom vars (p, args) htm m =
  if p = "="
  then try let hl, hr = dest_eq htm in itlist2 (unify_fo_ho_term vars) args [hl; hr] m
       with _ -> raise Unify
  else unify_fo_ho_term vars (Term.Fn (p, args)) htm m

let unify_fo_ho_literal vars (pol, atom) htm m =
  let htm' = if pol then htm else try dest_neg htm with _ -> raise Unify in
  unify_fo_ho_atom vars atom htm' m

end


module Metis_rules = struct

(* move a literal in the proof of a disjunction to the first position
   may not preserve the order of the other literals *)
let FRONT lit thm =
  let conc = concl thm in
  let disj = disjuncts (concl thm) in
  let rest = match partition (fun l -> l = lit) disj with
      ([], _) -> failwith "FRONT: literal not in disjunction"
    | (_ , r) -> r in
  let disj' = lit :: rest in
  let conc' = list_mk_disj disj' in
  let eq = DISJ_ACI_RULE (mk_eq (conc, conc')) in
  (PURE_ONCE_REWRITE_RULE [eq] thm, rest)

(* resolve two clauses, where atom has to appear at the first position of
   both clauses: positive in the first and negative in the second clause *)
let RESOLVE_N =
  let RESOLVE_1  = TAUT `!a. a ==> ~a ==> F`
  and RESOLVE_2L = TAUT `!a b. a \/ b ==> ~a ==> b`
  and RESOLVE_2R = TAUT `!a c. a ==> ~a \/ c ==> c`
  and RESOLVE_3  = TAUT `!a b c. a \/ b ==> ~a \/ c ==> b \/ c` in
  fun atom -> function
  ([], []) -> SPEC atom RESOLVE_1
| (r1, []) -> SPECL [atom; list_mk_disj r1] RESOLVE_2L
| ([], r2) -> SPECL [atom; list_mk_disj r2] RESOLVE_2R
| (r1, r2) -> SPECL [atom; list_mk_disj r1; list_mk_disj r2] RESOLVE_3

(* resolve two clauses th1 and th2, where atom appears somewhere
   positive in th1 and negative in th2 *)
let RESOLVE atom th1 th2 =
  (*print_endline ("Atom: " ^ string_of_term atom);
  print_endline ("th1 : " ^ string_of_term (concl th1));
  print_endline ("th2 : " ^ string_of_term (concl th2));*)
  try let (th1', r1) = FRONT atom th1
  and (th2', r2) = FRONT (mk_neg atom) th2 in
  let res = RESOLVE_N atom (r1, r2) in
  MP (MP res th1') th2'
  with _ -> failwith "resolve"

(* given A,  tm |- C, prove A |- ~tm \/ C or
   given A, ~tm |- C, prove A |-  tm \/ C *)
let DISCH_DISJ =
  let IMPL_NOT_L = TAUT `!a b. ~a ==> b <=>  a \/ b`
  and IMPL_NOT_R = TAUT `!a b.  a ==> b <=> ~a \/ b` in
  fun tm th ->
    let impl = DISCH tm th
    and (tm', IMPL_NOT) =
      try dest_neg tm, IMPL_NOT_L
      with _ ->    tm, IMPL_NOT_R in
    let eq = SPECL [tm'; concl th] IMPL_NOT in
    PURE_ONCE_REWRITE_RULE [eq] impl

(* given A, tm1, .., tmn |- th, prove A |- ~tm1 \/ .. \/ ~tmn \/ th *)
let DISCH_DISJS tms th = List.fold_right DISCH_DISJ tms th

end


module Metis_reconstruct2 = struct

open Metis_prover

let term_eq_mod_type t1 t2 tyinsts =
  try
    let _,tminsts,tyinsts = term_type_unify t1 t2 ([], [], tyinsts) in
    if !metisverb then
    begin
      Format.printf "unified with |tminsts| = %d!\n%!" (List.length tminsts);
      List.iter (fun t1, t2 -> Format.printf "%s <- %s\n%!" (string_of_term t1) (string_of_term t2)) tminsts
    end;
    assert (tminsts = []);
    Some tyinsts
  with _ -> None

let rec match_elems f m = function
    ([], []) -> [m]
  | ([],  _) -> []
  | (x :: xs, ys) -> List.map (fun y -> match f x y m with
        Some m' -> match_elems f m' (xs, List.filter ((!=) y) ys)
      | None -> []) ys |> List.concat

let match_fo_ho_clause vars = match_elems
  (fun ft ht m -> try Some (Metis_unify.unify_fo_ho_literal vars ft ht m) with Metis_unify.Unify -> None)
  []


let string_of_tminst = String.concat ", " o
  map (fun (tm, v) -> string_of_term tm ^ " <- " ^ string_of_term v)

let string_of_tyinst = String.concat ", " o
  map (fun (ty, v) -> string_of_type ty ^ " <- " ^ string_of_type v)

let string_of_instantiation (it, tminst, tyinst) =
  "([" ^ string_of_tminst tminst ^ "], [" ^ string_of_tyinst tyinst ^ "])"

let reorient_tysubst vars sub =
  let sub' = map (fun (ty, v) ->
    if List.mem v vars && is_vartype ty then v, ty else ty, v) sub in
  map (fun (ty, v) -> tysubst sub' ty, v) sub'

let rec hol_of_thm axioms fth =
  if !metisverb then Format.printf "hol_of_thm: %s\n%!" (Thm.toString fth);
  let env = Preterm.env_of_ths axioms in
  let hth = match Proof.thmToInference fth with
    Proof.Axiom clause ->
      let clausel = Literal.Set.toList clause in
      let maxs = Utils.List.concat_map (fun ax ->
        (*if !metisverb then Format.printf "ax: %s\n%!" (string_of_thm ax);*)
        let disjs = concl ax |> striplist dest_disj in
        (*if !metisverb then Format.printf "before matching\n%!";*)
        let tmvars = freesl (hyp ax) in
        let ms = match_fo_ho_clause tmvars (clausel, disjs) in
        (*if !metisverb then Format.printf "after matching\n%!";*)
        map (fun m -> m, ax) ms) axioms in
      assert (List.length maxs > 0);
      let tminst = List.map (fun v, tm -> mk_var (Metis_mapping.prefix v, type_of tm), tm) in
      if !metisverb then Format.printf "length maxs = %d\n%!" (List.length maxs);
      if !metisverb then List.iter (fun (m, ax) -> Format.printf "max: %s with m = %s\n%!" (string_of_thm ax) (string_of_tminst (tminst m))) maxs;
      let (m, ax) = List.hd maxs in
      INST (tminst m) ax
  (* Caution: the substitution can contain elements such as "x -> f(x)" *)
  | Proof.Subst (fsub, fth1) ->
      let th1 = hol_of_thm axioms fth1 in
      if !metisverb then Format.printf "subst with th1 = %s\n%!" (string_of_thm th1);

      let fsubl = Substitute.toList fsub in
      if !metisverb then Format.printf "before substitution lifting\n%!";
      let hsub = map (fun (v, t) -> t, Term.Var v) fsubl |>
        Metis_mapping.hol_of_substitution env in
      if !metisverb then Format.printf "subst: %s\n%!" (string_of_tminst hsub);
      let tyinst = itlist (fun (t, v) m ->
        let v' = find (fun v' -> name_of v' = name_of v) (frees (concl th1)) in
        type_unify (type_of v) (type_of v') m) hsub [] in
      let tminst = map (fun (t, v) -> inst tyinst t, inst tyinst v) hsub in

      if !metisverb then
        Format.printf "before instantiate of th1 = %s with %s\n%!"
          (string_of_thm th1) (string_of_instantiation ([], tminst, tyinst));

      INSTANTIATE ([], tminst, tyinst) th1
  | Proof.Resolve (atom, fth1, fth2) ->
      let th1 = hol_of_thm axioms fth1
      and th2 = hol_of_thm axioms fth2 in
      let env = Preterm.env_of_ths [th1; th2] @ env in
      if !metisverb then List.iter (fun (s, pty) -> Format.printf "%s <- %s\n%!" s (string_of_type (type_of_pretype pty))) env;
      if !metisverb then Format.printf "before resolving\n%!";
      if !metisverb then Format.printf "th1 = %s\n%!" (string_of_thm th1);
      if !metisverb then Format.printf "th2 = %s\n%!" (string_of_thm th2);
      let tm1 = striplist dest_disj (concl th1) |> List.filter (not o is_neg)
      and tm2 = striplist dest_disj (concl th2) |> List.filter is_neg |> List.map dest_neg in
      if !metisverb then List.iter (Format.printf "tm1: %s\n%!" o string_of_term) tm1;
      if !metisverb then List.iter (Format.printf "tm2: %s\n%!" o string_of_term) tm2;
      let hatom = Metis_mapping.hol_of_atom env atom in
      if !metisverb then Format.printf "hatom: %s\n%!" (string_of_term hatom);
      let cands = Utils.List.concat_map (fun x ->
        match term_eq_mod_type hatom x [] with
          None -> []
        | Some m -> Utils.List.filter_map (fun y -> term_eq_mod_type hatom y m) tm2) tm1 in
      if !metisverb then Format.printf "%d candidates available\n%!" (List.length cands);
      assert (List.length cands > 0);
      assert (let h = List.hd cands in List.for_all ((=) h) cands);
      let tyinsts = List.hd cands in
      let tyvars = map hyp axioms |> List.concat |>
        map type_vars_in_term |> List.concat in
      if !metisverb then Format.printf "Reorienting type substitution ...\n%!";
      let tyinsts = reorient_tysubst tyvars tyinsts in

      if !metisverb then Format.printf "Resolving ...\n%!";

      Metis_rules.RESOLVE (inst tyinsts hatom)
        (INST_TYPE tyinsts th1) (INST_TYPE tyinsts th2)
  | Proof.Refl term -> REFL (Metis_mapping.hol_of_term env term)
  | Proof.Assume atom -> SPEC (Metis_mapping.hol_of_atom env atom) EXCLUDED_MIDDLE
  | Proof.Equality (flit, fpath, ft) ->
      let hlit = Metis_mapping.hol_of_literal env flit in
      let fs, hpath = Metis_path.hol_of_literal_path flit fpath in
      let hs = follow_path hpath hlit in
      let ht = Metis_mapping.hol_of_term env ft in
      let m = type_unify (type_of ht) (type_of hs) [] in
      let hlit, hs, ht = inst m hlit, inst m hs, inst m ht in

      if !metisverb then begin
        Format.printf "Trying to replace %s : %s with %s : %s\n%!"
          (string_of_term hs) (string_of_type (type_of hs))
          (string_of_term ht) (string_of_type (type_of ht));
        Format.printf "In %s\n%!" (string_of_term hlit)
      end;

      let heq = mk_eq (hs, ht) in
      let conv = PATH_CONV hpath (PURE_ONCE_REWRITE_CONV [ASSUME heq]) in
      let hlit' = CONV_RULE conv (ASSUME hlit) in
      if !metisverb then Format.printf "hlit = %s, hlit' = %s\n%!"
        (string_of_term hlit) (string_of_thm hlit');

      if hs <> ht then assert (concl hlit' <> hlit);
      (try Metis_rules.DISCH_DISJS [heq; hlit] hlit'
      with _ -> failwith "equality")
  in
    (* eliminate duplicates in clause *)
    let hth = CONV_RULE DISJ_CANON_CONV hth in
    if !metisverb then begin
      Format.printf "hol_of_thm finished\n%!";
      let hth' = Thm.clause fth |> Literal.Set.toList |> Metis_mapping.hol_of_clause env in
      Format.printf "hol_of_thm returned:\n%s\n for\n%s\n%!"
        (string_of_term (concl hth)) (string_of_term hth')
    end;
    hth

end

(* ========================================================================= *)
(* Conversion of HOL to Metis FOL.                                           *)
(* ========================================================================= *)

module Metis_generate = struct

open Metis_prover

let metis_name = string_of_int

let rec metis_of_term env consts tm =
  if is_var tm && not (mem tm consts) then
    (Term.Var(metis_name (Meson.fol_of_var tm)))
  else (
    let f,args = strip_comb tm in
    if mem f env then failwith "metis_of_term: higher order" else
    let ff = Meson.fol_of_const f in
    Term.Fn (metis_name ff, map (metis_of_term env consts) args))

let metis_of_atom env consts tm =
  try let (l, r) = dest_eq tm in
      let l' = metis_of_term env consts l
      and r' = metis_of_term env consts r in
      Atom.mkEq (l', r')
  with Failure _ ->
      let f,args = strip_comb tm in
      if mem f env then failwith "metis_of_atom: higher order" else
      let ff = Meson.fol_of_const f in
      (metis_name ff, map (metis_of_term env consts) args)

let metis_of_literal env consts tm =
  let (pol, tm') = try (false, dest_neg tm)
     with Failure _ -> (true,           tm)
  in (pol, metis_of_atom env consts tm')

let metis_of_clause th =
  let lconsts = freesl (hyp th) in
  let tm = concl th in
  let hlits = disjuncts tm in
  let flits = map (metis_of_literal [] lconsts) hlits in
  let set = Literal.Set.fromList flits in
  Thm.axiom set

let metis_of_clauses = map metis_of_clause

end


(* ========================================================================= *)
(* Main Metis module.                                                        *)
(* ========================================================================= *)

module Metis = struct

open Metis_prover

(* ------------------------------------------------------------------------- *)
(* Some parameters controlling Metis behaviour.                              *)
(* ------------------------------------------------------------------------- *)

let split_limit = ref 0;; (* Limit of case splits before Metis proper  *)

(* ----------------------------------------------------------------------- *)
(* Basic HOL Metis procedure.                                              *)
(* ----------------------------------------------------------------------- *)

(* Debugging tactic. *)
let PRINT_TAC g = print_goal g; ALL_TAC g
let PRINT_ID_TAC s g = print_endline s; PRINT_TAC g

(* Slightly modified tactic from meson.ml. *)
let FOL_PREPARE_TAC ths =
  (* We start with a single goal: P. *)

  REFUTE_THEN ASSUME_TAC THEN
  (*PRINT_ID_TAC "refuted" THEN*)
  (*   0 [`~P`]

     `F`
   *)

  Meson.POLY_ASSUME_TAC (map GEN_ALL ths) THEN
  (*PRINT_ID_TAC "poly_assumed" THEN*)
  (*   0 [`~P`]
       1 [th1]
       ...
       n [thn]

     `F`
  *)

  W(MAP_EVERY(UNDISCH_TAC o concl o snd) o fst) THEN
  (* `~P ==> th1 ==> ... ==> thn ==> F` *)

  SELECT_ELIM_TAC THEN
  (* eliminate "select terms", e.g. Hilbert operators *)

  W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
  (*PRINT_ID_TAC "all-quantified" THEN*)
  (* MAP_EVERY is mapM for tactics
     I believe that this all-quantifies all free variables in the goal *)

  CONV_TAC(PRESIMP_CONV THENC
           TOP_DEPTH_CONV BETA_CONV THENC
           LAMBDA_ELIM_CONV THENC
           CONDS_CELIM_CONV THENC
           Meson.QUANT_BOOL_CONV) THEN
  (*PRINT_ID_TAC "converted" THEN*)

  REPEAT(GEN_TAC ORELSE DISCH_TAC) THEN
  (* remove outermost all-quantifiers (GEN_TAC) and implications (DISCH_TAC),
     moving them into assumptions *)

  REFUTE_THEN ASSUME_TAC THEN
  (* move conclusion negated into assumptions, replace goal by `F`*)

  RULE_ASSUM_TAC(CONV_RULE(NNF_CONV THENC SKOLEM_CONV)) THEN
  (* transform assumptions to NNF and skolemize *)

  REPEAT (FIRST_X_ASSUM CHOOSE_TAC) THEN
  (* remove existentials at the front *)

  ASM_FOL_TAC THEN
  (* fix function arities, e.g. f(x) and f(x,y) become I f x and I (I f x) y *)

  Meson.SPLIT_TAC (!split_limit) THEN
  RULE_ASSUM_TAC(CONV_RULE(PRENEX_CONV THENC WEAK_CNF_CONV)) THEN

  RULE_ASSUM_TAC(repeat
   (fun th -> SPEC(genvar(type_of(fst(dest_forall(concl th))))) th)) THEN
  (* destroy all-quantifiers and replace quantified variables by fresh ones *)

  REPEAT (FIRST_X_ASSUM (Meson.CONJUNCTS_THEN' ASSUME_TAC)) THEN
  (* make every conjunction a separate assumption *)

  RULE_ASSUM_TAC(CONV_RULE(ASSOC_CONV DISJ_ASSOC))
  (* associate disjunctions to the right *)

  (*THEN PRINT_ID_TAC "before Metis"*)


let without_warnings f =
  let tiv = !type_invention_warning in
  let reset () = type_invention_warning := tiv in
  type_invention_warning := false;
  try let y = f () in reset (); y
  with e -> (reset(); raise e)


let SIMPLE_METIS_REFUTE ths =
  Meson.clear_contrapos_cache();
  (* TODO: Metis currently uses randomness to search for proof --
     we should make that deterministic for proof reconstruction! *)
  Random.init 0;
  let rules = Metis_generate.metis_of_clauses ths in
  if !metisverb then
  begin
    Format.printf "Original ths:\n%!";
    List.iter (Format.printf "%s\n%!" o string_of_thm) ths
  end;
  let res = Loop.run rules in
  if !metisverb then Thm.print_proof res;
  let ths = map (CONV_RULE DISJ_CANON_CONV) ths in
  let proof = without_warnings (fun () -> Metis_reconstruct2.hol_of_thm ths res) in
  if !metisverb then
  begin
    Format.printf "ths:\n%!";
    List.iter (fun t -> print_thm t; Format.printf "\n%!") ths;
    Format.printf "Metis theorem:\n%!";
    print_thm proof;
    Format.printf "Metis end.\n%!";
  end;
  let allhyps = List.concat (List.map hyp ths) in
  assert (forall (fun h -> mem h allhyps) (hyp proof));
  assert (concl proof = `F`);
  proof

let PURE_METIS_TAC g =
  Meson.reset_vars(); Meson.reset_consts();
  (FIRST_ASSUM CONTR_TAC ORELSE
   W(ACCEPT_TAC o SIMPLE_METIS_REFUTE o map snd o fst)) g

let GEN_METIS_TAC ths =
  FOL_PREPARE_TAC ths THEN PURE_METIS_TAC

end
;;

(* ========================================================================= *)
(* Basic Metis refutation procedure and parametrized tactic.                 *)
(* ========================================================================= *)

let ASM_METIS_TAC = Metis.GEN_METIS_TAC;;

let METIS_TAC ths = POP_ASSUM_LIST(K ALL_TAC) THEN ASM_METIS_TAC ths;;

let METIS ths tm = prove(tm,METIS_TAC ths);;