exception UnificationFailure of string Lazy.t;;
-let unification vars locked_vars t1 t2 =
- let lookup = Subst.lookup_subst in
- let rec occurs_check subst what where =
- match where with
- | Terms.Var i when i = what -> true
- | Terms.Var _ ->
- let t = lookup where subst in
- if t <> where then occurs_check subst what t else false
- | Terms.Node l -> List.exists (occurs_check subst what) l
- | _ -> false
- in
- let rec unif subst vars s t =
- let s = match s with Terms.Var _ -> lookup s subst | _ -> s
- and t = match t with Terms.Var _ -> lookup t subst | _ -> t
-
+module Founif (B : Terms.Blob) = struct
+ module Subst = Subst.Subst(B)
+
+ let unification vars locked_vars t1 t2 =
+ let lookup = Subst.lookup_subst in
+ let rec occurs_check subst what where =
+ match where with
+ | Terms.Var i when i = what -> true
+ | Terms.Var _ ->
+ let t = lookup where subst in
+ if t <> where then occurs_check subst what t else false
+ | Terms.Node l -> List.exists (occurs_check subst what) l
+ | _ -> false
in
- match s, t with
- | s, t when s = t -> subst, vars
- | Terms.Var i, Terms.Var j
- when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
- raise
- (UnificationFailure (lazy "Inference.unification.unif"))
- | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
- unif subst vars t s
- | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
- unif subst vars t s
- | Terms.Var i, t when occurs_check subst i t ->
- raise
- (UnificationFailure (lazy "Inference.unification.unif"))
- | Terms.Var i, t when (List.mem i locked_vars) ->
- raise
- (UnificationFailure (lazy "Inference.unification.unif"))
- | Terms.Var i, t ->
- let subst = Subst.buildsubst i t subst in
- subst, vars
- | _, Terms.Var _ -> unif subst vars t s
- | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
- raise (UnificationFailure (lazy "Inference.unification.unif"))
- | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
- try
- List.fold_left2
- (fun (subst', vars) s t -> unif subst' vars s t)
- (subst, vars) tls tlt
- with Invalid_argument _ ->
+ let rec unif subst vars s t =
+ let s = match s with Terms.Var _ -> lookup s subst | _ -> s
+ and t = match t with Terms.Var _ -> lookup t subst | _ -> t
+
+ in
+ match s, t with
+ | s, t when s = t -> subst, vars
+ | Terms.Var i, Terms.Var j
+ when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
+ raise
+ (UnificationFailure (lazy "Inference.unification.unif"))
+ | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
+ unif subst vars t s
+ | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
+ unif subst vars t s
+ | Terms.Var i, t when occurs_check subst i t ->
+ raise
+ (UnificationFailure (lazy "Inference.unification.unif"))
+ | Terms.Var i, t when (List.mem i locked_vars) ->
+ raise
+ (UnificationFailure (lazy "Inference.unification.unif"))
+ | Terms.Var i, t ->
+ let subst = Subst.buildsubst i t subst in
+ subst, vars
+ | _, Terms.Var _ -> unif subst vars t s
+ | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
+ try
+ List.fold_left2
+ (fun (subst', vars) s t -> unif subst' vars s t)
+ (subst, vars) tls tlt
+ with Invalid_argument _ ->
+ raise (UnificationFailure (lazy "Inference.unification.unif"))
+ )
+ | _, _ ->
raise (UnificationFailure (lazy "Inference.unification.unif"))
- )
- | _, _ ->
- raise (UnificationFailure (lazy "Inference.unification.unif"))
- in
- let subst, vars = unif Subst.empty_subst vars t1 t2 in
- let vars = Subst.filter subst vars in
- subst, vars
+ in
+ let subst, vars = unif Subst.empty_subst vars t1 t2 in
+ let vars = Subst.filter subst vars in
+ subst, vars
+
+end
(* $Id$ *)
-module type Comparable =
- sig
- type t
- val is_eq : t -> t -> bool
- end
+module Index(B : Terms.Blob) = struct
+ module U = Terms.Utils(B)
-module C : Comparable =
- struct
- type t = NCic.term
- let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
- end
+ module ClauseOT =
+ struct
+ type t = Terms.direction * B.t Terms.unit_clause
+
+ let compare (d1,uc1) (d2,uc2) =
+ let c = Pervasives.compare d1 d2 in
+ if c <> 0 then c else U.compare_unit_clause uc1 uc2
+ ;;
+ end
- (*
-module C : Comparable =
- struct
- type t = Cic.term
- let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *)
- end
-*)
+ module ClauseSet :
+ Set.S with type elt = Terms.direction * B.t Terms.unit_clause
+ = Set.Make(ClauseOT)
-open Discrimination_tree
+ open Discrimination_tree
-module ClauseOT : Set.OrderedType
- with type t = Terms.direction * C.t Terms.unit_clause =
- struct
- type t = Terms.direction * C.t Terms.unit_clause
- let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) =
- Pervasives.compare (d1,id1) (d2,id2)
- end
+ module FotermIndexable : Indexable with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm
+ =
+ struct
-module ClauseSet = Set.Make(ClauseOT)
+ type input = B.t Terms.foterm
+ type constant_name = B.t
-module FotermIndexable : Indexable
-with type input = C.t Terms.foterm and
- type constant_name = C.t = struct
+ let path_string_of =
+ let rec aux arity = function
+ | Terms.Leaf a -> [Constant (a, arity)]
+ | Terms.Var i -> assert (arity = 0); [Variable]
+ | Terms.Node (Terms.Var _::_) -> assert false
+ | Terms.Node ([] | [ _ ] ) -> assert false
+ | Terms.Node (Terms.Node _::_) -> assert false
+ | Terms.Node (hd::tl) ->
+ aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
+ in
+ aux 0
+ ;;
-type input = C.t Terms.foterm
-type constant_name = C.t
+ let compare e1 e2 =
+ match e1,e2 with
+ | Constant (a1,ar1), Constant (a2,ar2) ->
+ let c = B.compare a1 a2 in
+ if c <> 0 then c else Pervasives.compare ar1 ar2
+ | Variable, Variable -> 0
+ | Constant _, Variable -> ~-1
+ | Variable, Constant _ -> 1
+ | Proposition, _ | _, Proposition
+ | Datatype, _ | _, Datatype
+ | Dead, _ | _, Dead
+ | Bound _, _ | _, Bound _ -> assert false
+ ;;
-let path_string_of =
- let rec aux arity = function
- | Terms.Leaf a -> [Constant (a, arity)]
- | Terms.Var i -> assert (arity = 0); [Variable]
- | Terms.Node (Terms.Var _::_) -> assert false
- | Terms.Node ([] | [ _ ] ) -> assert false
- | Terms.Node (Terms.Node _::_) -> assert false
- | Terms.Node (hd::tl) ->
- aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl)
- in
- aux 0
-;;
+ let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
-let compare e1 e2 =
- match e1,e2 with
- | Constant (a1,ar1), Constant (a2,ar2) ->
- if C.is_eq a1 a2 then Pervasives.compare ar1 ar2
- else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *)
- | _ -> Pervasives.compare e1 e2
-;;
+ end
-let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;;
+ module DT : DiscriminationTree with
+ type constant_name = B.t and
+ type input = B.t Terms.foterm and
+ type data = ClauseSet.elt and
+ type dataset = ClauseSet.t
+ = Make(FotermIndexable)(ClauseSet)
end
-
-module DiscriminationTree = Make(FotermIndexable)(ClauseSet)
(* $Id$ *)
-(* (weight of constants, [(meta, weight_of_meta)]) *)
-type weight = int * (int * int) list;;
-
-let string_of_weight (cw, mw) =
- let s =
- String.concat ", "
- (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
- in
- Printf.sprintf "[%d; %s]" cw s
-;;
-
-let weight_of_term term =
- let vars_dict = Hashtbl.create 5 in
- let rec aux = function
- | Terms.Var i ->
- (try
- let oldw = Hashtbl.find vars_dict i in
- Hashtbl.replace vars_dict i (oldw+1)
- with Not_found ->
- Hashtbl.add vars_dict i 1);
- 0
- | Terms.Leaf _ -> 1
- | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
- in
- let w = aux term in
- let l =
- Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
- in
- let compare w1 w2 =
- match w1, w2 with
- | (m1, _), (m2, _) -> m2 - m1
- in
- (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
-;;
-
-let compute_clause_weight = assert false (*
- let factor = 2 in
- match o with
- | Terms.Lt ->
- let w, m = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false right) in
- w + (factor * (List.length m)) ;
- | Terms.Le -> assert false
- | Terms.Gt ->
- let w, m = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false left) in
- w + (factor * (List.length m)) ;
- | Terms.Ge -> assert false
- | Terms.Eq
- | Terms.Incomparable ->
- let w1, m1 = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false right) in
- let w2, m2 = (weight_of_term
- ~consider_metas:true ~count_metas_occurrences:false left) in
- w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
-*)
-;;
-
-(* returns a "normalized" version of the polynomial weight wl (with type
- * weight list), i.e. a list sorted ascending by meta number,
- * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
- * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
- * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
-let normalize_weight maxmeta (cw, wl) =
- let rec aux = function
- | 0 -> []
- | m -> (m, 0)::(aux (m-1))
- in
- let tmpl = aux maxmeta in
- let wl =
- List.sort
- (fun (m, _) (n, _) -> Pervasives.compare m n)
- (List.fold_left
- (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
- in
- (cw, wl)
-;;
-
-
-let normalize_weights (cw1, wl1) (cw2, wl2) =
- let rec aux wl1 wl2 =
- match wl1, wl2 with
- | [], [] -> [], []
- | (m, w)::tl1, (n, w')::tl2 when m = n ->
- let res1, res2 = aux tl1 tl2 in
- (m, w)::res1, (n, w')::res2
- | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
- let res1, res2 = aux tl1 wl2 in
- (m, w)::res1, (m, 0)::res2
- | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
- let res1, res2 = aux wl1 tl2 in
- (n, 0)::res1, (n, w')::res2
- | [], (n, w)::tl2 ->
- let res1, res2 = aux [] tl2 in
- (n, 0)::res1, (n, w)::res2
- | (m, w)::tl1, [] ->
- let res1, res2 = aux tl1 [] in
- (m, w)::res1, (m, 0)::res2
- | _, _ -> assert false
- in
- let cmp (m, _) (n, _) = compare m n in
- let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
- (cw1, wl1), (cw2, wl2)
-;;
-
-(* Riazanov: 3.1.5 pag 38 *)
-(* TODO: optimize early detection of Terms.Incomparable case *)
-let compare_weights (h1, w1) (h2, w2) =
- let res, diffs =
- try
- List.fold_left2
- (fun ((lt, eq, gt), diffs) w1 w2 ->
- match w1, w2 with
- | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
- let diffs = (w1 - w2) + diffs in
- let r = compare w1 w2 in
- if r < 0 then (lt+1, eq, gt), diffs
- else if r = 0 then (lt, eq+1, gt), diffs
- else (lt, eq, gt+1), diffs
- | _ -> assert false)
- ((0, 0, 0), 0) w1 w2
- with Invalid_argument _ -> assert false
- in
- let hdiff = h1 - h2 in
- match res with
- | (0, _, 0) ->
- if hdiff < 0 then Terms.Lt
- else if hdiff > 0 then Terms.Gt
- else Terms.Eq
- | (m, _, 0) ->
- if hdiff <= 0 then Terms.Lt
- else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
- | (0, _, m) ->
- if hdiff >= 0 then Terms.Gt
- else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
- | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
- | _ -> assert false
-;;
-
-
-let rec aux_ordering t1 t2 =
- match t1, t2 with
- | Terms.Var _, _
- | _, Terms.Var _ -> Terms.Incomparable
-
- | Terms.Leaf a1, Terms.Leaf a2 ->
- let cmp = Pervasives.compare a1 a2 in
- if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
-
- | Terms.Leaf _, Terms.Node _ -> Terms.Lt
- | Terms.Node _, Terms.Leaf _ -> Terms.Gt
-
- | Terms.Node l1, Terms.Node l2 ->
- let rec cmp t1 t2 =
- match t1, t2 with
- | [], [] -> Terms.Eq
- | _, [] -> Terms.Gt
- | [], _ -> Terms.Lt
- | hd1::tl1, hd2::tl2 ->
- let o = aux_ordering hd1 hd2 in
- if o = Terms.Eq then cmp tl1 tl2
- else o
- in
- cmp l1 l2
-;;
-
-let nonrec_kbo t1 t2 =
- let w1 = weight_of_term t1 in
- let w2 = weight_of_term t2 in
- let w1, w2 = normalize_weights w1 w2 in
- match compare_weights w1 w2 with
- | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
- | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
- | Terms.Eq -> aux_ordering t1 t2
- | res -> res
-;;
-
-(*
-let rec kbo t1 t2 =
- let aux = aux_ordering ~recursion:false in
- let w1 = weight_of_term t1
- and w2 = weight_of_term t2 in
- let rec cmp t1 t2 =
+module Orderings (B : Terms.Blob) = struct
+
+ type weight = int * (int * int) list;;
+
+ let string_of_weight (cw, mw) =
+ let s =
+ String.concat ", "
+ (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
+ in
+ Printf.sprintf "[%d; %s]" cw s
+ ;;
+
+ let weight_of_term term =
+ let vars_dict = Hashtbl.create 5 in
+ let rec aux = function
+ | Terms.Var i ->
+ (try
+ let oldw = Hashtbl.find vars_dict i in
+ Hashtbl.replace vars_dict i (oldw+1)
+ with Not_found ->
+ Hashtbl.add vars_dict i 1);
+ 0
+ | Terms.Leaf _ -> 1
+ | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
+ in
+ let w = aux term in
+ let l =
+ Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
+ in
+ let compare w1 w2 =
+ match w1, w2 with
+ | (m1, _), (m2, _) -> m2 - m1
+ in
+ (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
+ ;;
+
+ let compute_clause_weight = assert false (*
+ let factor = 2 in
+ match o with
+ | Terms.Lt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ w + (factor * (List.length m)) ;
+ | Terms.Le -> assert false
+ | Terms.Gt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ w + (factor * (List.length m)) ;
+ | Terms.Ge -> assert false
+ | Terms.Eq
+ | Terms.Incomparable ->
+ let w1, m1 = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ let w2, m2 = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+ *)
+ ;;
+
+ (* returns a "normalized" version of the polynomial weight wl (with type
+ * weight list), i.e. a list sorted ascending by meta number,
+ * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
+ * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
+ * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
+ let normalize_weight maxmeta (cw, wl) =
+ let rec aux = function
+ | 0 -> []
+ | m -> (m, 0)::(aux (m-1))
+ in
+ let tmpl = aux maxmeta in
+ let wl =
+ List.sort
+ (fun (m, _) (n, _) -> Pervasives.compare m n)
+ (List.fold_left
+ (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
+ in
+ (cw, wl)
+ ;;
+
+
+ let normalize_weights (cw1, wl1) (cw2, wl2) =
+ let rec aux wl1 wl2 =
+ match wl1, wl2 with
+ | [], [] -> [], []
+ | (m, w)::tl1, (n, w')::tl2 when m = n ->
+ let res1, res2 = aux tl1 tl2 in
+ (m, w)::res1, (n, w')::res2
+ | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
+ let res1, res2 = aux tl1 wl2 in
+ (m, w)::res1, (m, 0)::res2
+ | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
+ let res1, res2 = aux wl1 tl2 in
+ (n, 0)::res1, (n, w')::res2
+ | [], (n, w)::tl2 ->
+ let res1, res2 = aux [] tl2 in
+ (n, 0)::res1, (n, w)::res2
+ | (m, w)::tl1, [] ->
+ let res1, res2 = aux tl1 [] in
+ (m, w)::res1, (m, 0)::res2
+ | _, _ -> assert false
+ in
+ let cmp (m, _) (n, _) = compare m n in
+ let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
+ (cw1, wl1), (cw2, wl2)
+ ;;
+
+ (* Riazanov: 3.1.5 pag 38 *)
+ (* TODO: optimize early detection of Terms.Incomparable case *)
+ let compare_weights (h1, w1) (h2, w2) =
+ let res, diffs =
+ try
+ List.fold_left2
+ (fun ((lt, eq, gt), diffs) w1 w2 ->
+ match w1, w2 with
+ | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
+ let diffs = (w1 - w2) + diffs in
+ let r = compare w1 w2 in
+ if r < 0 then (lt+1, eq, gt), diffs
+ else if r = 0 then (lt, eq+1, gt), diffs
+ else (lt, eq, gt+1), diffs
+ | _ -> assert false)
+ ((0, 0, 0), 0) w1 w2
+ with Invalid_argument _ -> assert false
+ in
+ let hdiff = h1 - h2 in
+ match res with
+ | (0, _, 0) ->
+ if hdiff < 0 then Terms.Lt
+ else if hdiff > 0 then Terms.Gt
+ else Terms.Eq
+ | (m, _, 0) ->
+ if hdiff <= 0 then Terms.Lt
+ else if (- diffs) >= hdiff then Terms.Le else Terms.Incomparable
+ | (0, _, m) ->
+ if hdiff >= 0 then Terms.Gt
+ else if diffs >= (- hdiff) then Terms.Ge else Terms.Incomparable
+ | (m, _, n) when m > 0 && n > 0 -> Terms.Incomparable
+ | _ -> assert false
+ ;;
+
+
+ let rec aux_ordering t1 t2 =
match t1, t2 with
- | [], [] -> Terms.Eq
- | _, [] -> Terms.Gt
- | [], _ -> Terms.Lt
- | hd1::tl1, hd2::tl2 ->
- let o =
- kbo hd1 hd2
+ | Terms.Var _, _
+ | _, Terms.Var _ -> Terms.Incomparable
+
+ | Terms.Leaf a1, Terms.Leaf a2 ->
+ let cmp = Pervasives.compare a1 a2 in
+ if cmp = 0 then Terms.Eq else if cmp < 0 then Terms.Lt else Terms.Gt
+
+ | Terms.Leaf _, Terms.Node _ -> Terms.Lt
+ | Terms.Node _, Terms.Leaf _ -> Terms.Gt
+
+ | Terms.Node l1, Terms.Node l2 ->
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Terms.Eq
+ | _, [] -> Terms.Gt
+ | [], _ -> Terms.Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o = aux_ordering hd1 hd2 in
+ if o = Terms.Eq then cmp tl1 tl2
+ else o
in
- if o = Terms.Eq then cmp tl1 tl2
- else o
- in
- let w1, w2 = normalize_weights w1 w2 in
- let comparison = compare_weights w1 w2 in
- match comparison with
- | Terms.Le ->
- let r = aux t1 t2 in
- if r = Terms.Lt then Terms.Lt
- else if r = Terms.Eq then (
- match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
- | _, _ -> Terms.Incomparable
- ) else Terms.Incomparable
- | Terms.Ge ->
- let r = aux t1 t2 in
- if r = Terms.Gt then Terms.Gt
- else if r = Terms.Eq then (
- match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
- | _, _ -> Terms.Incomparable
- ) else Terms.Incomparable
- | Terms.Eq ->
- let r = aux t1 t2 in
- if r = Terms.Eq then (
- match t1, t2 with
- | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
- cmp tl1 tl2
- | _, _ -> Terms.Incomparable
- ) else r
- | res -> res
-;;
-*)
-
-let compare_terms = nonrec_kbo;;
-
+ cmp l1 l2
+ ;;
+
+ let nonrec_kbo t1 t2 =
+ let w1 = weight_of_term t1 in
+ let w2 = weight_of_term t2 in
+ let w1, w2 = normalize_weights w1 w2 in
+ match compare_weights w1 w2 with
+ | Terms.Le -> if aux_ordering t1 t2 = Terms.Lt then Terms.Lt else Terms.Incomparable
+ | Terms.Ge -> if aux_ordering t1 t2 = Terms.Gt then Terms.Gt else Terms.Incomparable
+ | Terms.Eq -> aux_ordering t1 t2
+ | res -> res
+ ;;
+
+ (*
+ let rec kbo t1 t2 =
+ let aux = aux_ordering ~recursion:false in
+ let w1 = weight_of_term t1
+ and w2 = weight_of_term t2 in
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Terms.Eq
+ | _, [] -> Terms.Gt
+ | [], _ -> Terms.Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o =
+ kbo hd1 hd2
+ in
+ if o = Terms.Eq then cmp tl1 tl2
+ else o
+ in
+ let w1, w2 = normalize_weights w1 w2 in
+ let comparison = compare_weights w1 w2 in
+ match comparison with
+ | Terms.Le ->
+ let r = aux t1 t2 in
+ if r = Terms.Lt then Terms.Lt
+ else if r = Terms.Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Terms.Lt then Terms.Lt else Terms.Incomparable
+ | _, _ -> Terms.Incomparable
+ ) else Terms.Incomparable
+ | Terms.Ge ->
+ let r = aux t1 t2 in
+ if r = Terms.Gt then Terms.Gt
+ else if r = Terms.Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Terms.Gt then Terms.Gt else Terms.Incomparable
+ | _, _ -> Terms.Incomparable
+ ) else Terms.Incomparable
+ | Terms.Eq ->
+ let r = aux t1 t2 in
+ if r = Terms.Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ cmp tl1 tl2
+ | _, _ -> Terms.Incomparable
+ ) else r
+ | res -> res
+ ;;
+ *)
+
+ let compare_terms = nonrec_kbo;;
+
+end
projects / helm.git / commitdiff