Some fixes in range module

src/basic/FStar.Compiler.Range.Ops.fst

@@ -23,28 +23,31 @@ friend FStar.Compiler.Range.Type
 open FStar.Json
 open FStar.Compiler.Effect 
 open FStar.Compiler.Util
+open FStar.Class.Ord
 
 module Options = FStar.Options
 
 let union_rng r1 r2 =
-  if r1.file_name <> r2.file_name then r2
-  else let start_pos =
-           if pos_geq r1.start_pos r2.start_pos then
-             r2.start_pos
-           else r1.start_pos in
-       let end_pos =
-           if pos_geq r1.end_pos r2.end_pos then
-             r1.end_pos
-           else r2.end_pos in
-       mk_rng r1.file_name start_pos end_pos
+  if r1.file_name <> r2.file_name
+  then r2
+  else
+    let start_pos = min r1.start_pos r2.start_pos in
+    let end_pos   = max r1.end_pos   r2.end_pos in
+    mk_rng r1.file_name start_pos end_pos
+
 let union_ranges r1 r2 = {
   def_range=union_rng r1.def_range r2.def_range;
   use_range=union_rng r1.use_range r2.use_range
 }
+
+(* is r1 included in r2? *)
 let rng_included r1 r2 =
-    if r1.file_name <> r2.file_name then false
-    else pos_geq r1.start_pos r2.start_pos &&
-         pos_geq r2.end_pos r1.end_pos
+  if r1.file_name <> r2.file_name
+  then false
+  else
+    r2.start_pos <=? r1.start_pos &&
+    r2.end_pos >=? r1.end_pos
+
 let string_of_pos pos =
     format2 "%s,%s" (string_of_int pos.line) (string_of_int pos.col)
 let string_of_file_name f =
@@ -95,7 +98,8 @@ let compare_rng r1 r2     =
 let compare r1 r2 = compare_rng r1.def_range r2.def_range
 let compare_use_range r1 r2 = compare_rng r1.use_range r2.use_range
 let range_before_pos m1 p =
-    pos_geq p (end_of_range m1)
+    p >=? end_of_range m1
+
 let end_of_line p = {p with col=max_int}
 let extend_to_end_of_line r = mk_range (file_of_range r)
                                        (start_of_range r)
@@ -122,16 +126,16 @@ let json_of_def_range r =
             (end_of_range r)
 
 let intersect_rng r1 r2 =
-  if r1.file_name <> r2.file_name then r2
-  else let start_pos =
-           if pos_geq r1.start_pos r2.start_pos then
-             r1.start_pos
-           else r2.start_pos in
-       let end_pos =
-           if pos_geq r1.end_pos r2.end_pos then
-             r2.end_pos
-           else r1.end_pos in
-       mk_rng r1.file_name start_pos end_pos
+  if r1.file_name <> r2.file_name
+  then r2
+  else
+    let start_pos = max r1.start_pos r2.start_pos in
+    let end_pos   = min r1.end_pos   r2.end_pos in
+    (* If start_pos > end_pos, then the intersection is empty, just take the bound *)
+    if start_pos >=? end_pos
+    then r2
+    else mk_rng r1.file_name start_pos end_pos
+
 let intersect_ranges r1 r2 = {
   def_range=intersect_rng r1.def_range r2.def_range;
   use_range=intersect_rng r1.use_range r2.use_range

src/basic/FStar.Compiler.Range.Type.fst

@@ -16,6 +16,9 @@
 module FStar.Compiler.Range.Type
 
 open FStar.Compiler.Effect 
+open FStar.Class.Deq
+open FStar.Class.Ord
+open FStar.Compiler.Order
 
 [@@ PpxDerivingYoJson; PpxDerivingShow ]
 type file_name = string
@@ -26,9 +29,16 @@ type pos = {
   col: int
 }
 let max i j = if i < j then j else i
-let pos_geq p1 p2 =
-   (p1.line > p2.line ||
-   (p1.line = p2.line && p1.col >= p2.col))
+
+let compare_pos (p1 p2 : pos) : order =
+  lex (cmp p1.line p2.line) (fun _ -> cmp p1.col p2.col)
+
+instance deq_pos : deq pos = { (=?) = (=); }
+
+instance ord_pos : ord pos = {
+  super = deq_pos;
+  cmp = compare_pos;
+}
 
 [@@ PpxDerivingYoJson; PpxDerivingShow ]
 type rng = {

src/basic/FStar.Compiler.Range.Type.fsti

@@ -16,6 +16,8 @@
 module FStar.Compiler.Range.Type
 
 open FStar.Compiler.Effect
+open FStar.Class.Deq
+open FStar.Class.Ord
 
 [@@ PpxDerivingYoJson; PpxDerivingShow]
 new val rng : Type0
@@ -26,6 +28,9 @@ new val range : Type0
 [@@ PpxDerivingYoJson; PpxDerivingShow]
 new val pos : Type0
 
+instance val deq_pos : deq pos
+instance val ord_pos : ord pos
+
 val dummy_rng : rng
 val mk_rng : string -> pos -> pos -> rng
 

src/class/FStar.Class.Ord.fst

@@ -9,6 +9,9 @@ let (<=?) x y = cmp x y <> Gt
 let (>?)  x y = cmp x y =  Gt
 let (>=?) x y = cmp x y <> Lt
 
+let min x y = if x <=? y then x else y
+let max x y = if x >=? y then x else y
+
 instance ord_eq (a:Type) (d : ord a) : Tot (deq a) = d.super
 
 let rec insert (#a:Type) {| ord a |} (x:a) (xs:list a) : list a =

src/class/FStar.Class.Ord.fsti

@@ -29,6 +29,9 @@ val (<=?) : #a:Type -> {| ord a |} -> a -> a -> bool
 val (>?)  : #a:Type -> {| ord a |} -> a -> a -> bool
 val (>=?) : #a:Type -> {| ord a |} -> a -> a -> bool
 
+val min : #a:Type -> {| ord a |} -> a -> a -> a
+val max : #a:Type -> {| ord a |} -> a -> a -> a
+
 instance val ord_int    : ord int
 instance val ord_bool   : ord bool
 instance val ord_unit   : ord unit