snapshot

[helm.git] / helm / software / components / ng_paramodulation / nCicBlob.ml

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 7cd4e5762f7d57c61c9caf179b9af64865ae4a1f..09399b3261b2d634352c54cc63b95614b898fb0b 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -27,10 +27,22 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
   let rec compare x y = 
     match x,y with
     | NCic.Rel i, NCic.Rel j -> i-j
+    | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
     | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
-    | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *)
+    | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+    | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+    | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+    | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+    | NCic.Appl _, NCic.Meta _ -> ~-1
+    | NCic.Meta _, NCic.Appl _ -> 1
     | _ -> assert false
   ;;
+  
+  let compare x y = 
+    if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 
+    else compare x y
+  ;;
 
   let pp t = 
     NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;