;;
-
-
let print_subst ?(prefix="\n") subst =
String.concat prefix
(List.map
| Eq -> "="
| Incomparable -> "I"
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
module OrderedTerm =
struct
type t = Cic.term
aux term
;;
+let rec remove_local_context =
+ function
+ | Cic.Meta (i,_) -> Cic.Meta (i,[])
+ | Cic.Appl l ->
+ Cic.Appl(List.map remove_local_context l)
+ | t -> t
+
(************************* rpo ********************************)
let number = [
module IntSet = Set.Make(OrderedInt)
+let compute_equality_weight (ty,left,right,o) =
+ let factor = 2 in
+ match o with
+ | Lt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false right) in
+ w + (factor * (List.length m)) ;
+ | Le -> assert false
+ | Gt ->
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false left) in
+ w + (factor * (List.length m)) ;
+ | Ge -> assert false
+ | Eq
+ | 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))
+;;
+
+(* old
let compute_equality_weight (ty,left,right,o) =
let metasw = ref 0 in
let weight_of t =
(* let w = weight_of (Cic.Appl [ty;left;right]) in *)
w + !metasw
;;
-
+*)
(* returns a "normalized" version of the polynomial weight wl (with type
* weight list), i.e. a list sorted ascending by meta number,
| (m, _, n) when m > 0 && n > 0 ->
Incomparable
| _ -> assert false
-
;;
| Right -> "Right"
;;
+let metas_of_term t =
+ List.map fst (CicUtil.metas_of_term t)
+;;
-let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
-let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
-let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
-let eq_XURI () =
- let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
- UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())