interval.mlw

module Bound
     type t = Strict | Large

end

module Convexe
  use bool.Bool
  use option.Option
  use q.Q as Q
  use Bound
  use real.RealInfix

  type t =
  | Finite Q.t Bound.t Q.t Bound.t
  | InfFinite Q.t Bound.t
  | FiniteInf Q.t Bound.t
  | Inf

  type t' = { a: t }
   invariant {
     match a with
     | Inf | InfFinite _ _ | FiniteInf _ _ -> true
     | Finite minv minb maxv maxb ->
       if Q.(equal minv maxv)
       then minb = Bound.Large /\ maxb = Bound.Large
       else Q.(minv < maxv)
     end
   }

   predicate cmp (x:real) (b:Bound.t) (y:real) =
     match b with
     | Bound.Large -> x <=. y
     | Bound.Strict -> x <. y
     end

   predicate mem (x:real) (e:t') =
   match e.a with
   | Inf -> true
   | InfFinite v b  -> cmp x b v
   | FiniteInf v b  -> cmp v b x
   | Finite v b v' b'  -> cmp v b x /\ cmp x b' v'
   end

  let lemma exists_mem (e:t') : real
    ensures { mem result e } =
    match e.a with
    | Inf -> 0.
    | InfFinite v _ -> v.Q.real -. 1.
    | FiniteInf v _ -> v.Q.real +. 1.
    | Finite v _ v' _  ->
        0.75 *. v.Q.real +. 0.25 *. v'.Q.real
    end

  let is_singleton e
      ensures { forall q. mem q e -> (forall q'. mem q' e -> q = q') -> match result with | Some q'' -> mem q'' e | None -> false end }
      ensures { (exists q q'. not (Q.equal q q') /\ mem q e /\ mem q' e) -> result = None }
  =
   match e.a with
   | Inf -> assert { mem 0. e }; assert { mem 1. e }; None
   | InfFinite v _     -> assert { mem (v.Q.real -. 2.) e }; assert { mem (v.Q.real -. 1.) e }; None
   | FiniteInf v _     -> assert { mem (v.Q.real +. 2.) e }; assert { mem (v.Q.real +. 1.) e }; None
   | Finite v b v' b'  -> if Q.(v = v') then begin
        assert { b = Bound.Large /\ b' = Bound.Large };
        assert { forall q. mem q e -> q = v.Q.real };
        Some v
       end else begin
        let ghost c = 0.75 *. v.Q.real +. 0.25 *. v'.Q.real in
        let ghost c' = 0.25 *. v.Q.real +. 0.75 *. v'.Q.real in
        assert { cmp v b c }; assert { cmp c b' v'};
        assert { cmp v b c' }; assert { cmp c' b' v'};
        assert { mem c e }; assert { mem c' e };
        None
     end
   end

  let singleton q
      ensures { result.a = Finite q Bound.Large q Bound.Large }
      ensures { mem q result }
      ensures { forall q'. mem q' result -> q.Q.real = q' }
  =
    { a = Finite q Bound.Large q Bound.Large }


  let except e x
    ensures {
     forall q. mem q e -> q <> x.Q.real ->
      match result with
       | Some res -> mem q res
       | None -> false
      end 
     }
   =
    match e.a with
    | Inf
    | InfFinite _ Strict
    | FiniteInf _ Strict -> Some e
    | InfFinite v Large -> if Q.(v = x) then Some {a=InfFinite v Strict} else Some e
    | FiniteInf v Large -> if Q.(v = x) then Some {a=FiniteInf v Strict} else Some e
    | Finite _ Strict _ Strict -> Some e
    | Finite v Strict v' Large -> if Q.(v' = x) then Some {a=Finite v Strict v' Strict} else Some e
    | Finite v Large v' Strict -> if Q.(v = x) then Some {a=Finite v Strict v' Strict} else Some e
    | Finite v Large v' Large ->
      let is_min = Q.(v = x) in
      let is_max = Q.(v' = x) in
      if is_min && is_max then None
      else if is_min
      then Some {a = Finite v Strict v' Large }
      else if is_max
      then Some {a = Finite v Large v' Strict }
      else Some e
      end

  type is_comparable =
  | Gt
  | Lt
  | Ge
  | Le
  | Uncomparable

  use q.Ord as Ord

  let is_comparable e1 e2
    ensures {
      match result with
      | Uncomparable -> true
      | Lt -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <. q2
      | Gt -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 >. q2
      | Le -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <=. q2
      | Ge -> forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 >=. q2
    end
    }
   =
    match e1.a, e2.a with
    | Inf, Inf
    | Inf, _
    | _, Inf
    | InfFinite _ _, InfFinite _ _
    | FiniteInf _ _, FiniteInf _ _ -> Uncomparable
    | FiniteInf v1 b1, InfFinite v2 b2
    | Finite v1 b1 _ _, InfFinite v2 b2
    | FiniteInf v1 b1, Finite _ _ v2 b2 ->
      match Q.compare v1 v2 with
      | Ord.Eq ->
         match b1, b2 with
         | Large, Large -> Ge
         | _ -> Gt
         end
      | Ord.Lt -> Uncomparable
      | Ord.Gt -> Gt
      end
    | Finite _ _ v1 b1, FiniteInf v2 b2
    | InfFinite v1 b1, FiniteInf v2 b2
    | InfFinite v1 b1, Finite v2 b2 _ _ ->
       match Q.compare v1 v2 with
       | Ord.Eq ->
         match b1, b2 with
         | Large, Large -> Le
         | _ -> Lt
         end
       | Ord.Lt -> Lt
       | Ord.Gt ->  Uncomparable
       end
    | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
       match Q.compare v1' v2, Q.compare v1 v2' with
       | Ord.Eq, _ ->
         match b1', b2 with
         | Large, Large -> Le
         | _ -> Lt
         end
       | _, Ord.Eq ->
         match b1, b2' with
         | Large, Large -> Ge
         | _ -> Gt
         end
       | Ord.Lt, _ -> Lt
       | _, Ord.Gt -> Gt
       | _ -> Uncomparable
     end
    end



  let is_distinct e1 e2
   ensures { result -> (forall q1 q2. mem q1 e1 -> mem q2 e2 -> q1 <> q2) }
  =
    match is_comparable e1 e2 with
    | Uncomparable | Le | Ge -> false
    | _ -> true
    end


  let is_included e1 e2
   ensures { result -> (forall q. mem q e1 -> mem q e2) }
   =
    match e1.a, e2.a with
    | Inf, Inf -> true
    | Inf, _
    | InfFinite _ _ , (FiniteInf _ _ | Finite _ _ _ _)
    | FiniteInf _ _ , (InfFinite _ _ | Finite _ _ _ _) -> false
    | _, Inf -> true
    | InfFinite v1 b1, InfFinite v2 b2
    | Finite _ _ v1 b1, InfFinite v2 b2 ->
        match Q.compare v1 v2 with
        | Ord.Eq ->
         match b1, b2 with
         | Large, Strict -> false
         | _ -> true
         end
        | Ord.Lt -> true
        | Ord.Gt -> false
        end
    | FiniteInf v1 b1, FiniteInf v2 b2
    | Finite v1 b1 _ _, FiniteInf v2 b2 ->
        match Q.compare v1 v2 with
        | Ord.Eq ->
         match b1, b2 with
         | Large, Strict -> false
         | _ -> true
         end
        | Ord.Lt -> false
        | Ord.Gt -> true
        end
    | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
        match Q.compare v2 v1, Q.compare v1' v2', b1, b2, b1', b2' with
        | Ord.Eq, _, Large, Strict, _,_ -> false
        | _, Ord.Eq, _,_, Large, Strict -> false   
        | (Ord.Lt | Ord.Eq), (Ord.Lt | Ord.Eq), _, _, _, _ -> true
        | _ -> false
        end
     end

   let cmp (x:Q.t) (b:Bound.t) (y:Q.t) =
     match b with
     | Bound.Large -> Q.(x <= y)
     | Bound.Strict -> Q.(x < y)
     end

   let mem (x:Q.t) (e:t')
     ensures { result = mem x.Q.real e } =
   match e.a with
   | Inf -> true
   | InfFinite v b  -> cmp x b v
   | FiniteInf v b  -> cmp v b x
   | Finite v b v' b'  -> andb (cmp v b x) (cmp x b' v')
   end

   let absent (x:Q.t) (e:t')
     ensures { result = not (mem x.Q.real e) } =
     notb (mem x e)

  let mult_pos q e
     requires { Q.(0. <. q.real) }
     ensures { forall q'. mem q' e -> mem (q.Q.real *. q') result }
   =
     assert { forall a b. (q.Q.real *. a) <. (q.Q.real *. b) <-> a <. b };
     assert { forall a b. (q.Q.real *. a) <=. (q.Q.real *. b) <-> a <=. b };
     match e.a with
     | Inf -> { a = Inf }
     | InfFinite v b  -> { a = InfFinite Q.(q*v) b }
     | FiniteInf v b  -> { a = FiniteInf Q.(q*v) b }
     | Finite v b v' b'  ->
     { a = Finite Q.(q*v) b Q.(q*v') b' }
     end

  let mult_neg q e
     requires { Q.(q.real <. 0.) }
     ensures { forall q'. mem q' e -> mem (q.Q.real *. q') result }
   =
     assert { forall a b. (q.Q.real *. a) >. (q.Q.real *. b) <-> a <. b };
     assert { forall a b. (q.Q.real *. a) >=. (q.Q.real *. b) <-> a <=. b };
     match e.a with
     | Inf -> { a = Inf }
     | InfFinite v b  -> { a = FiniteInf Q.(q*v) b }
     | FiniteInf v b  -> { a = InfFinite Q.(q*v) b }
     | Finite v b v' b'  -> { a = Finite Q.(q*v') b' Q.(q*v) b }
     end

  let mult_cst c e
       ensures { forall q. mem q e -> mem (c.Q.real *. q) result }
   =
    if Q.(c = (of_int 0))    then singleton (Q.of_int 0)
    else if Q.(of_int 0 < c) then mult_pos c e
    else                          mult_neg c e

  let add_cst q e
     ensures { forall q'. mem q' e -> mem (q.Q.real +. q') result }
   =
     match e.a with
     | Inf -> { a = Inf }
     | InfFinite v b  -> { a = InfFinite Q.(q+v) b }
     | FiniteInf v b  -> { a = FiniteInf Q.(q+v) b }
     | Finite v b v' b'  -> { a = Finite Q.(q+v) b Q.(q+v') b' }
     end

  let add_bound b1 b2
    ensures { forall c d c' d'. cmp c b1 d -> cmp c' b2 d' -> cmp (c+.c') result (d +. d') } 
    ensures { b1 = Large -> b2 = Large -> result = Large }
   =
    match b1, b2 with
    | Large, Large -> Large
    | Large, Strict -> Strict
    | Strict, Large -> Strict
    | Strict, Strict -> Strict
    end

  let add e1 e2
     ensures { forall q1 q2. mem q1 e1 -> mem q2 e2 -> mem (q1 +. q2) result }
   =
     match e1.a, e2.a with
     | Inf, _ | _, Inf -> { a = Inf }
     | InfFinite _ _, FiniteInf _ _ | FiniteInf _ _, InfFinite _ _ -> { a = Inf }
     | InfFinite v1 b1, (InfFinite v2 b2 | Finite _ _ v2 b2)
     | Finite _ _ v2 b2, InfFinite v1 b1
      -> { a = InfFinite Q.(v1+v2) (add_bound b1 b2) }
     | FiniteInf v1 b1, (FiniteInf v2 b2 | Finite v2 b2 _ _)
     | Finite v2 b2 _ _, FiniteInf v1 b1
      -> { a = FiniteInf Q.(v1+v2) (add_bound b1 b2) }
     | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
        { a = Finite Q.(v1+v2) (add_bound b1 b2) Q.(v1'+v2') (add_bound b1' b2') }
     end

  let minus e1 e2
     ensures { forall q1 q2. mem q1 e1 -> mem q2 e2 -> mem (q1 -. q2) result }
  =
    add e1 (mult_neg Q.(of_int (-1)) e2)

  let gt c
    ensures { forall q. mem q result <-> q >. c }
   =
    { a = FiniteInf c Strict }

  let ge c
    ensures { forall q. mem q result <-> q >=. c }
   =
    { a = FiniteInf c Large }

  let lt c
    ensures { forall q. mem q result <-> q <. c }
   =
    { a = InfFinite c Strict }

  let le c
    ensures { forall q. mem q result <-> q <=. c }
   =
    { a = InfFinite c Large }

  let gt' c
    ensures { forall q. mem q result <-> (exists c. mem c result /\ q >. c) }
  =
    match c.a with
     | Finite v _ _ _ -> { a = FiniteInf v Strict }
     | InfFinite _ _ -> { a = Inf }
     | FiniteInf _ Strict -> c
     | FiniteInf v Large -> { a = FiniteInf v Strict }
     | Inf -> { a = Inf }
     end

  let ge' c
    ensures { forall q. mem q result <-> (exists c. mem c result /\ q >=. c) }
  =
   match c.a with
     | Finite v b _ _ -> { a = FiniteInf v b }
     | InfFinite _ _ -> { a = Inf }
     | FiniteInf _ _-> c
     | Inf -> { a = Inf }
     end

  let lt' c
    ensures { forall q. mem q result <-> (exists c. mem c result /\ q <. c) }
  =
   match c.a with
     | Finite _ _ v _ -> { a = InfFinite v Strict }
     | InfFinite _ Strict -> c
     | InfFinite v Large -> { a = InfFinite v Strict }
     | FiniteInf _ _-> { a = Inf }
     | Inf -> { a = Inf }
     end

  let le' c
    ensures { forall q. mem q result <-> (exists c. mem c result /\ q <=. c) }
  =
   match c.a with
     | Finite _ _ v b -> { a = InfFinite v b }
     | InfFinite _ _ -> c
     | FiniteInf _ _-> { a = Inf }
     | Inf -> { a = Inf }
     end

  let min_bound_sup v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
    ensures { forall q. (cmp q b1 v1 /\ cmp q b2 v2) <-> cmp q b3 v3 }
    ensures { Q.(v3 <= v1) } ensures { Q.(v3 <= v2) }
    ensures { b1 = Large -> b2 = Large -> b3 = Large }
  =
    match Q.compare v1 v2, b1, b2 with
    | Ord.Eq, Large, Large -> (v1,Large)
    | Ord.Eq, _ ,_  -> (v1,Strict)
    | Ord.Lt, _, _  -> (v1,b1)
    | Ord.Gt, _ ,_  -> (v2,b2)
    end

  let min_bound_inf v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
    ensures { forall q. (cmp v1 b1 q \/ cmp v2 b2 q) <-> cmp v3 b3 q }
    ensures { Q.(v3 <= v1) } ensures { Q.(v3 <= v2) }
    ensures { b1 = Large -> b2 = Large -> b3 = Large }
  =
    match Q.compare v1 v2, b1, b2 with
    | Ord.Eq, Strict, Strict -> (v1,Strict)
    | Ord.Eq, _, _ -> (v1,Large)
    | Ord.Lt, _, _ -> (v1,b1)
    | Ord.Gt, _, _ -> (v2,b2)
    end

  let max_bound_sup v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
    ensures { forall q. (cmp q b1 v1 \/ cmp q b2 v2) <-> cmp q b3 v3 }
    ensures { Q.(v1 <= v3) } ensures { Q.(v2 <= v3) }
    ensures { b1 = Large -> b2 = Large -> b3 = Large }
  =
    match Q.compare v1 v2, b1, b2 with
    | Ord.Eq, Strict, Strict -> (v1,Strict)
    | Ord.Eq, _, _ -> (v1,Large)
    | Ord.Lt, _, _ -> (v2,b2)
    | Ord.Gt, _, _ -> (v1,b1)
    end

  let max_bound_inf v1 b1 v2 b2: (v3:Q.t,b3:Bound.t)
    ensures { forall q. (cmp v1 b1 q /\ cmp v2 b2 q) <-> cmp v3 b3 q }
    ensures { Q.(v1 <= v3) } ensures { Q.(v2 <= v3) }
    ensures { b1 = Large -> b2 = Large -> b3 = Large }
  =
    match Q.compare v1 v2, b1, b2 with
    | Ord.Eq, Large, Large -> (v1,Large)
    | Ord.Eq, _, _ -> (v1,Strict)
    | Ord.Lt, _, _ -> (v2,b2)
    | Ord.Gt, _, _ -> (v1,b1)
    end

  let union e1 e2
     ensures { forall q. mem q e1 -> mem q result }
     ensures { forall q. mem q e2 -> mem q result }
   =
     match e1.a, e2.a with
     | Inf, _ | _, Inf -> { a = Inf }
     | InfFinite _ _, FiniteInf _ _ | FiniteInf _ _, InfFinite _ _ -> { a = Inf }
     | InfFinite v1 b1, (InfFinite v2 b2 | Finite _ _ v2 b2)
     | Finite _ _ v2 b2, InfFinite v1 b1
      ->
      let v3,b3 = max_bound_sup v1 b1 v2 b2 in
      { a = InfFinite v3 b3 }
     | FiniteInf v1 b1, (FiniteInf v2 b2 | Finite v2 b2 _ _)
     | Finite v2 b2 _ _, FiniteInf v1 b1
     -> let v3,b3 = min_bound_inf v1 b1 v2 b2 in
        { a = FiniteInf v3 b3 }
     | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
        let v3,b3 = min_bound_inf v1 b1 v2 b2 in
        let v4,b4 = max_bound_sup v1' b1' v2' b2' in
        { a = Finite v3 b3 v4 b4 }
     end

  predicate mem_bottom (q:real) (e:option t') =
    match e with
    | Some e -> mem q e
    | None -> false
    end

  lemma mem_bottom_som: forall q e [mem_bottom q (Some e)]. mem_bottom q (Some e) = mem q e

  let mk_finite v1 b1 v2 b2
    ensures { forall q. (cmp v1 b1 q /\ cmp q b2 v2) <-> mem_bottom q result }
    ensures { match result with
        | Some r -> r.a = (Finite v1 b1 v2 b2)
        | _ -> false
        end }
  =
   match Q.compare v1 v2 with
   | Ord.Eq ->
      match b1, b2 with
      | Large, Large  ->
         assert { forall q. cmp v1 b1 q -> cmp q b2 v2 -> q = v1.Q.real};
         Some { a = Finite v1 Large v2 Large }
      | _ -> None
      end
   | Ord.Lt -> Some { a = Finite v1 b1 v2 b2 }
   | Ord.Gt -> None
   end

  let inter e1 e2
     ensures { forall q. (mem q e1 /\ mem q e2) <-> mem_bottom q result }
   =
     match e1.a, e2.a with
     | Inf, _ -> Some e2
     | _, Inf -> Some e1
     | InfFinite v1 b1, FiniteInf v2 b2
     | FiniteInf v2 b2, InfFinite v1 b1 ->
        mk_finite v2 b2 v1 b1
     | InfFinite v1 b1, InfFinite v2 b2 ->
      let v3,b3 = min_bound_sup v1 b1 v2 b2 in
      Some { a = InfFinite v3 b3 }     
     | InfFinite v1 b1, Finite v2 b2 v3 b3
     | Finite v2 b2 v3 b3, InfFinite v1 b1
      ->
      let v4,b4 = min_bound_sup v1 b1 v3 b3 in
      mk_finite v2 b2 v4 b4
     | FiniteInf v1 b1, FiniteInf v2 b2 ->
      let v3,b3 = max_bound_inf v1 b1 v2 b2 in
      let r = { a = FiniteInf v3 b3 } in
      assert { forall q. mem q r -> cmp v3 b3 q };
      assert { forall q. cmp v3 b3 q -> cmp v1 b1 q };
      assert { forall q. cmp v1 b1 q -> mem q e1 };
      Some r
     | FiniteInf v1 b1, Finite v2 b2 v3 b3
     | Finite v2 b2 v3 b3, FiniteInf v1 b1
      ->
      let v4,b4 = max_bound_inf v1 b1 v2 b2 in
      mk_finite v4 b4 v3 b3
     | Finite v1 b1 v1' b1', Finite v2 b2 v2' b2' ->
        let v3,b3 = max_bound_inf v1 b1 v2 b2 in
        let v4,b4 = min_bound_sup v1' b1' v2' b2' in
        assert { forall q. mem q e1 -> mem q e2 -> cmp v3 b3 q };
        assert { forall q. mem q e1 -> mem q e2 -> cmp q b4 v4 };
        mk_finite v3 b3 v4 b4
     end

  let zero = let r = singleton Q.(of_int 0) in assert { forall q. mem q r <-> q = 0. }; r

  let reals = let r = {a=Inf} in assert { forall q. mem q r }; r

  let is_reals e
    ensures { result = (forall q. mem q e) }
   =
   match e.a with
   | Inf -> true
   | InfFinite v _     -> assert { not (mem (v.Q.real +. 1.) e) }; false
   | FiniteInf v _     -> assert { not (mem (v.Q.real -. 1.) e) }; false
   | Finite v _ _ _    -> assert { not (mem (v.Q.real -. 1.) e) }; false
   end

  let integers = reals

  use int.Int as Int
  use real.FromInt as FromInt

  let is_integer e
    ensures { result <-> (forall q. mem q e -> exists z. q = FromInt.from_int z) }
   =
   match e.a with
   | Finite v1 Large v2 Large    -> andb Q.(v1 = v2) Int.(v1.Q.den = 1)
   | Inf
   | InfFinite _ _
   | FiniteInf _ _
   | Finite _ _ _ _ -> false
   end


  let choose e
    ensures { mem result e }
   =
    match e.a with
   | Inf -> Q.(of_int 0)
   | InfFinite v Large
   | FiniteInf v Large
   | Finite v Large _ _
   | Finite _ _ v Large    -> v
   | InfFinite v Strict    -> Q.(v - (of_int 1)) 
   | FiniteInf v Strict    -> Q.(v + (of_int 1))
   | Finite v1 Strict v2 Strict ->
     let half = Q.make 1 2 in
     Q.(v1 * half + v2 * half)
   end

  type split_heuristic =
    | Singleton Q.t
    | Splitted t' t'
    | NotSplitted

  let split_heuristic c
    ensures { forall q. mem q c -> match result with
                        | Singleton q' -> q = q'
                        | Splitted c1 c2 -> mem q c1 \/ mem q c2
                        | NotSplitted -> true
                        end
                        }
   =
    let qzero = Q.of_int 0 in
    let zero = singleton qzero in
    match c.a with
    | Inf -> Splitted { a = InfFinite qzero Strict } { a = FiniteInf qzero Large }
    | InfFinite v b ->
      match Q.compare qzero v, b with
      | Ord.Eq, Large ->
        Splitted { a = InfFinite qzero Strict } zero
      | Ord.Eq, Strict
      | Ord.Gt, _  -> NotSplitted
      | Ord.Lt, _ ->
        Splitted { a = InfFinite qzero Strict } { a = Finite qzero Large v b }
      end
    | FiniteInf v b ->
      match Q.compare v qzero, b with
      | Ord.Eq, Large ->
        Splitted zero { a = FiniteInf v Strict }
      | Ord.Eq, Strict
      | Ord.Gt, _  -> NotSplitted
      | Ord.Lt, _ ->
        Splitted { a = Finite v b qzero Strict } { a = FiniteInf qzero Large }
      end
    | Finite v1 b1 v2 b2 ->
      match Q.compare v1 qzero, b1, Q.compare v2 qzero, b2, Q.compare v1 v2 with
      | _, _, _, _, Ord.Eq ->
        Singleton v1
      | Ord.Eq, Large, _, _, _ ->
        Splitted zero { a = Finite qzero Strict v2 b2 }
      | _, _, Ord.Eq, Large, _ ->
        Splitted { a = Finite v1 b1 qzero Strict } zero
      | _ ->
        let half = Q.make 1 2 in
        let m = Q.(half * v1 + half * v2) in
        Splitted { a = Finite v1 b1 m Strict } { a = Finite m Large v2 b2 }
      end
    end

end