Skip to content
Snippets Groups Projects
Commit af9218d5 authored by François Bobot's avatar François Bobot
Browse files

New union

parent 79a8d4d6
No related branches found
No related tags found
1 merge request!20Better reccursive function handling
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 1718 additions and 1274 deletions
dolmen @ 38294b2d
Compare 660c77c8...38294b2d
Subproject commit 660c77c855d8b7441f6aec56c84c54e46229bc15 Subproject commit 38294b2dcb07477506b9a06e4a51d1fdb2c8c3e6
src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
+ 1
− 1
View file @ af9218d5
;; produced by local colibri2.drv ;; ;; produced by local colibri2.drv ;;
(set-logic ALL) (set-logic ALL)
(set-info :smt-lib-version 2.6) (set-info :smt-lib-version 2.6)
(set-option :max-steps-colibri2 10000) (set-option :max-steps-colibri2 11000)
(declare-datatypes ((tuple2 2)) (declare-datatypes ((tuple2 2))
((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2)))))) ((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2))))))
......
src_colibri2/theories/quantifier/pattern.ml
+ 1
− 1
View file @ af9218d5
...@@ -250,7 +250,7 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t = ...@@ -250,7 +250,7 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
in in
let nodes = let nodes =
IArray.foldi_non_empty_exn IArray.foldi_non_empty_exn
~f:(fun i acc parg -> Node.S.inter acc (get_parents (i + 1) parg)) ~f:(fun i acc parg -> Node.S.inter acc (get_parents i parg))
~init:(get_parents 0) pargs ~init:(get_parents 0) pargs
in in
if Node.S.is_empty nodes then raise Not_found else nodes if Node.S.is_empty nodes then raise Not_found else nodes
......
src_colibri2/theories/quantifier/quantifier.ml
+ 3
− 2
View file @ af9218d5
...@@ -298,8 +298,9 @@ let th_register d = ...@@ -298,8 +298,9 @@ let th_register d =
(* let delay = Events.Delayed_by 10 in *) (* let delay = Events.Delayed_by 10 in *)
Daemon.attach_reg_sem d Ground.ClosedQuantifier.key quantifier_registered; Daemon.attach_reg_sem d Ground.ClosedQuantifier.key quantifier_registered;
Ground.register_converter d (fun d g -> Ground.register_converter d (fun d g ->
if not (application_useless d g) then add_info_on_ground_terms d g if application_useless d g then
else Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g); Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g
else add_info_on_ground_terms d g);
Interp.Register.check_closed_quantifier d (fun d g -> Interp.Register.check_closed_quantifier d (fun d g ->
let n = Ground.ClosedQuantifier.node g in let n = Ground.ClosedQuantifier.node g in
let unknown = let unknown =
......
src_colibri2/theories/quantifier/trigger.ml
+ 3
− 2
View file @ af9218d5
...@@ -356,12 +356,13 @@ let instantiate d tri subst = ...@@ -356,12 +356,13 @@ let instantiate d tri subst =
Expr.Term.Var.M.map (Egraph.find_def d) subst.Ground.Subst.term; Expr.Term.Var.M.map (Egraph.find_def d) subst.Ground.Subst.term;
} }
in in
Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a" Debug.dprintf9 debug
"[Quant] %a instantiation found %a, pat %a, checks:%a, eager:%b"
Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form Ground.Subst.pp subst Ground.ClosedQuantifier.pp tri.form
Fmt.(list ~sep:comma Pattern.pp) Fmt.(list ~sep:comma Pattern.pp)
tri.pats tri.pats
Fmt.(list ~sep:comma Pattern.pp) Fmt.(list ~sep:comma Pattern.pp)
tri.checks; tri.checks tri.eager;
if if
tri.eager tri.eager
&& List.for_all && List.for_all
......
src_common/union.mlw
+ 357
− 112
View file @ af9218d5
...@@ -6,113 +6,177 @@ module Union ...@@ -6,113 +6,177 @@ module Union
use interval.Bound use interval.Bound
use real.RealInfix use real.RealInfix
type t0 = type on =
| Singleton Q.t t0 | OnSin Q.t on
| Inter Q.t Bound.t Q.t Bound.t t0 | OnEnd Q.t Bound.t off
| FiniteInf Q.t Bound.t | OnInf
| End
with off =
| OffSin Q.t off
| OffEnd Q.t Bound.t on
| OffInf
type t = type t =
| InfFinite Q.t Bound.t t0 | On on
| Finite t0 | Off off
| Inf
function length_on (l:on) : int =
match l with
| OnSin _ l ->
length_on l + 1
| OnEnd _ _ l ->
length_off l + 1
| OnInf -> 0
end
with length_off (l:off) : int =
match l with
| OffSin _ l ->
length_off l + 1
| OffEnd _ _ l ->
length_on l + 1
| OffInf -> 0
end
function length0 (l:t0) : int = let rec lemma pos_length_on (l:on)
ensures { length_on l >= 0 } =
match l with match l with
| Singleton _ l -> | OnSin _ l -> pos_length_on l
length0 l + 1 | OnEnd _ _ l ->
| Inter _ _ _ _ l -> pos_length_off l
length0 l + 2 | OnInf -> ()
| FiniteInf _ _ ->
1
| End -> 0
end end
let rec lemma length0_positive (l:t0) with lemma pos_length_off (l:off)
ensures { length0 l >= 0 } = ensures { length_off l >= 0 } =
match l with match l with
| Singleton _ l -> length0_positive l | OffSin _ l -> pos_length_off l
| Inter _ _ _ _ l -> | OffEnd _ _ l ->
length0_positive l pos_length_on l
| FiniteInf _ _ -> () | OffInf -> ()
| End -> ()
end end
function length (l:t) : int = function length (l:t) : int =
match l with match l with
| InfFinite _ _ l -> | On l ->
length0 l + 1 length_on l + 1
| Finite l -> | Off l ->
length0 l length_off l
| Inf ->
0
end end
predicate lt_bound0 (x:Q.t) (l:t0) = predicate lt_bound_on (x:Q.t) (l:on) =
match l with match l with
| Singleton q l -> | OnSin q l ->
x <. q /\ lt_bound0 x l x <. q /\ lt_bound_on x l
| Inter q _ q' _ l -> | OnEnd q _ l ->
x <. q /\ x <. q' /\ lt_bound0 x l x <. q /\ lt_bound_off x l
| FiniteInf q _ -> | OnInf -> true
x <. q
| End -> true
end end
let rec ghost lt_bound0_transitive (x:Q.t) (y:Q.t) (l:t0) (m:t0) with lt_bound_off (x:Q.t) (l:off) =
requires { forall q. lt_bound0 q l -> q <. x } match l with
| OffSin q l ->
x <. q /\ lt_bound_off x l
| OffEnd q _ l ->
x <. q /\ lt_bound_on x l
| OffInf -> true
end
let rec ghost lt_bound_on_on_transitive (x:Q.t) (y:Q.t) (l:on) (m:on)
requires { forall q. lt_bound_on q l -> q <. x }
requires { x <=. y }
requires { lt_bound_on y m }
ensures { forall q. lt_bound_on q l -> lt_bound_on q m }
variant { m } =
match m with
| OnSin _ m ->
lt_bound_on_on_transitive x y l m
| OnEnd _ _ m ->
lt_bound_on_off_transitive x y l m
| OnInf -> ()
end
with ghost lt_bound_on_off_transitive (x:Q.t) (y:Q.t) (l:on) (m:off)
requires { forall q. lt_bound_on q l -> q <. x }
requires { x <=. y }
requires { lt_bound_off y m }
ensures { forall q. lt_bound_on q l -> lt_bound_off q m }
variant { m } =
match m with
| OffSin _ m ->
lt_bound_on_off_transitive x y l m
| OffEnd _ _ m ->
lt_bound_on_on_transitive x y l m
| OffInf -> ()
end
let rec ghost smaller_lt_bound_on (x:Q.t) (y:Q.t) (m:on)
requires { x <=. y }
requires { lt_bound_on y m }
ensures { lt_bound_on x m }
variant { m } =
match m with
| OnSin _ m ->
smaller_lt_bound_on x y m
| OnEnd _ _ m ->
smaller_lt_bound_off x y m
| OnInf -> ()
end
with ghost smaller_lt_bound_off (x:Q.t) (y:Q.t) (m:off)
requires { x <=. y } requires { x <=. y }
requires { lt_bound0 y m } requires { lt_bound_off y m }
ensures { forall q. lt_bound0 q l -> lt_bound0 q m } ensures { lt_bound_off x m }
variant { m } = variant { m } =
match m with match m with
| Singleton _ m -> | OffSin _ m ->
lt_bound0_transitive x y l m smaller_lt_bound_off x y m
| Inter _ _ _ _ m -> | OffEnd _ _ m ->
lt_bound0_transitive x y l m smaller_lt_bound_on x y m
| FiniteInf _ _ -> () | OffInf -> ()
| End -> ()
end end
predicate lt_bound (x:Q.t) (l:t) = predicate lt_bound (x:Q.t) (l:t) =
match l with match l with
| InfFinite q _ l -> | On l -> lt_bound_on x l
x <. q \/ lt_bound0 x l | Off l -> lt_bound_off x l
| Finite l -> end
lt_bound0 x l
| Inf -> predicate ordered_on (l:on) =
true match l with
| OnSin q l ->
lt_bound_on q l /\
ordered_on l
| OnEnd q _ l ->
lt_bound_off q l /\
ordered_off l
| OnInf -> true
end end
predicate ordered0 (l:t0) = with ordered_off (l:off) =
match l with match l with
| Singleton q l -> | OffSin q l ->
lt_bound0 q l /\ lt_bound_off q l /\
ordered0 l ordered_off l
| Inter q _ q' _ l -> | OffEnd q _ l ->
Q.(q < q') /\ lt_bound_on q l /\
lt_bound0 q' l /\ ordered_on l
ordered0 l | OffInf -> true
| FiniteInf _ _ -> true
| End -> true
end end
predicate ordered (l:t) = predicate ordered (l:t) =
match l with match l with
| InfFinite q _ l -> | On l -> ordered_on l
lt_bound0 q l /\ | Off l -> ordered_off l
ordered0 l
| Finite l ->
ordered0 l
| Inf -> true
end end
type t' = { a: t } type t' = { a: t }
invariant { ordered a } invariant { ordered a }
invariant { invariant {
a <> Finite End a <> Off OffInf
} }
by { a = Inf } by { a = On OnInf }
predicate cmp (x:real) (b:Bound.t) (y:real) = predicate cmp (x:real) (b:Bound.t) (y:real) =
match b with match b with
...@@ -120,66 +184,79 @@ module Union ...@@ -120,66 +184,79 @@ module Union
| Bound.Strict -> x <. y | Bound.Strict -> x <. y
end end
predicate mem0 (x:real) (l:t0) = predicate mem_on (x:real) (l:on) =
match l with match l with
| Singleton q l -> | OnSin q l ->
x = q \/ mem0 x l x <. q \/ (q <. x /\ mem_on x l)
| Inter q b q' b' l -> | OnEnd q b l ->
(cmp q b x /\ cmp x b' q') \/ mem0 x l cmp x b q \/ mem_off x l
| FiniteInf q b -> | OnInf -> true
cmp q b x
| End -> false
end end
let rec lemma lt_bound0_is_not_mem0 (q:Q.t) (r:real) (l:t0) with mem_off (x:real) (l:off) =
requires { lt_bound0 q l }
requires { r <=. q }
ensures { not (mem0 r l) }
=
match l with match l with
| Singleton _ l -> lt_bound0_is_not_mem0 q r l | OffSin q l ->
| Inter _ _ _ _ l -> x = q \/ mem_off x l
lt_bound0_is_not_mem0 q r l | OffEnd q b l ->
| FiniteInf _ _ -> () not (cmp x b q) /\ mem_on x l
| End -> () | OffInf -> false
end end
predicate mem (x:real) (l:t) = predicate mem (x:real) (l:t) =
match l with match l with
| InfFinite q b l -> | On l ->
cmp x b q \/ mem0 x l mem_on x l
| Finite l -> | Off l ->
mem0 x l mem_off x l
| Inf -> end
true
let rec ghost lt_bound_is_not_mem_off (q:Q.t) (l:off)
requires { lt_bound_off q l }
ensures { forall r. r <=. q -> not (mem_off r l) }
variant { l }
=
match l with
| OffSin _ l -> lt_bound_is_not_mem_off q l
| OffEnd _ _ _ -> ()
| OffInf -> ()
end end
let singleton (q:Q.t) : t' let singleton (q:Q.t) : t'
ensures { forall x:real. mem x result.a <-> x = q } ensures { forall x:real. mem x result.a <-> x = q }
= =
{ a = Finite (Singleton q End) } { a = Off (OffSin q OffInf) }
let is_singleton (u:t') : (option Q.t, ghost real, ghost real) let is_singleton (u:t') : (option Q.t, ghost real, ghost real)
ensures { ensures {
let (o,x1,x2) = result in let (o,x1,x2) = result in
match o with match o with
| Some q -> forall x:real. mem x u.a <-> x = q | Some q -> forall x:real. mem x u.a <-> x = q
| None -> x1 <> x2 /\ mem x1 u.a /\ mem x2 u.a | None -> x1 <> x2 /\ mem x1 u.a /\ mem x2 u.a
end end
} = } =
match u.a with match u.a with
| Inf -> (None, ghost 0., ghost 1.) | Off (OffSin q OffInf) -> (Some q,ghost 0.,ghost 1.)
| InfFinite q _ _ -> (None, ghost (Q.real q)-.1., ghost (Q.real q)-.2.) | Off (OffSin q (OffSin q' _)) -> (None,ghost Q.real q,ghost Q.real q')
| Finite (Singleton q End) -> (Some q,ghost 0., ghost 1.) | Off (OffSin _ (OffEnd q _ on)) ->
| Finite End -> absurd match on with
| Finite (Inter q _ q' _ _) -> | OnSin q' _ -> (None,ghost (Q.real q*.0.3+.Q.real q'*.0.7),
(None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75) ghost (Q.real q*.0.7+.Q.real q'*.0.3))
| Finite (FiniteInf q _) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.) | OnEnd q' _ _ -> (None,ghost(Q.real q*.0.3+.Q.real q'*.0.7),
| Finite (Singleton q (Singleton q' _)) -> ghost(Q.real q*.0.7+.Q.real q'*.0.3))
(None,ghost (Q.real q), ghost (Q.real q')) | OnInf -> (None,ghost(Q.real q+.1.),ghost(Q.real q+.2.))
| Finite (Singleton _ (Inter q _ q' _ _)) -> end
(None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75) | Off (OffEnd q _ on) ->
| Finite (Singleton _ (FiniteInf q _)) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.) match on with
| OnSin q' _ -> (None,ghost (Q.real q*.0.3+.Q.real q'*.0.7),
ghost (Q.real q*.0.7+.Q.real q'*.0.3))
| OnEnd q' _ _ -> (None,ghost(Q.real q*.0.3+.Q.real q'*.0.7),
ghost(Q.real q*.0.7+.Q.real q'*.0.3))
| OnInf -> (None,ghost(Q.real q+.1.),ghost(Q.real q+.2.))
end
| On (OnSin q _) -> (None, ghost (Q.real q-.1.), ghost (Q.real q-.2.))
| On (OnEnd q _ _) -> (None, ghost (Q.real q-.1.), ghost (Q.real q-.2.))
| On OnInf -> (None, ghost 0., ghost 1.)
| Off OffInf -> absurd
end end
use q.Ord as Ord use q.Ord as Ord
...@@ -236,6 +313,174 @@ module Union ...@@ -236,6 +313,174 @@ module Union
| Ord.Gt, _, _ -> (v1,b1) | Ord.Gt, _, _ -> (v1,b1)
end end
let inter (u:t') (v:t') : option t'
ensures {
forall x:real. (mem x u.a /\ mem x v.a) <->
match result with
| None -> false
| Some w -> mem x w.a
end
} =
let rec inter_on_on (u:on) (v:on) : on
requires { ordered_on u }
requires { ordered_on v }
ensures { ordered_on result }
ensures {
forall x:real. (mem_on x u /\ mem_on x v) <-> mem_on x result
}
ensures {
forall q.
(lt_bound_on q u) -> (lt_bound_on q v) ->
(lt_bound_on q result )
}
variant { length_on u + length_on v } =
match u, v with
| u, OnInf | OnInf, u -> u
| OnSin qu lu, OnSin qv lv ->
match Q.compare qu qv with
| Ord.Eq -> OnSin qu (inter_on_on lu lv)
| Ord.Lt -> smaller_lt_bound_on qu qv lv; OnSin qu (inter_on_on lu v)
| Ord.Gt -> smaller_lt_bound_on qv qu lu; OnSin qv (inter_on_on u lv)
end
| OnEnd qu bu lu, OnEnd qv bv lv ->
match Q.compare qu qv with
| Ord.Eq ->
let b = match bu, bv with
| Large, Large -> Large
| _ -> Strict
end
in
lt_bound_is_not_mem_off qu lv;
lt_bound_is_not_mem_off qu lu;
OnEnd qu b (inter_off_off lu lv)
| Ord.Lt -> smaller_lt_bound_off qu qv lv; OnEnd qu bu (inter_on_off v lu)
| Ord.Gt -> smaller_lt_bound_off qv qu lu; OnEnd qv bv (inter_on_off u lv)
end
| (OnSin qu lu) as u, (OnEnd qv bv lv) as v
| (OnEnd qv bv lv) as v, (OnSin qu lu) as u ->
match Q.compare qu qv with
| Ord.Eq -> smaller_lt_bound_on qv qu lu; OnEnd qv Strict (inter_on_off lu lv)
| Ord.Lt -> smaller_lt_bound_off qu qv lv; OnSin qu (inter_on_on lu v)
| Ord.Gt -> smaller_lt_bound_on qv qu lu; OnEnd qv bv (inter_on_off u lv)
end
end
with inter_on_off (u:on) (v:off) : off
requires { ordered_on u }
requires { ordered_off v }
ensures { ordered_off result }
ensures {
forall x:real. (mem_on x u /\ mem_off x v) <-> mem_off x result
}
ensures {
forall q.
(lt_bound_on q u) -> (lt_bound_off q v) ->
(lt_bound_off q result )
}
variant { length_on u + length_off v } =
match u, v with
| _, OffInf -> OffInf
| OnInf, u -> u
| OnSin qu lu, OffSin qv lv ->
match Q.compare qu qv with
| Ord.Eq -> inter_on_off lu lv
| Ord.Lt -> (inter_on_off lu v)
| Ord.Gt -> OffSin qv (inter_on_off u lv)
end
| OnEnd qu bu lu, OffEnd qv bv lv ->
match Q.compare qu qv with
| Ord.Eq ->
match bu, bv with
| Large, Large -> OffSin qu (inter_on_off lv lu)
| _ -> inter_on_off lv lu
end
| Ord.Lt -> inter_off_off lu v
| Ord.Gt -> smaller_lt_bound_off qv qu lu; OffEnd qv bv (inter_on_on u lv)
end
| (OnSin qu lu) as u, (OffEnd qv bv lv) as v ->
match Q.compare qu qv with
| Ord.Eq -> OffEnd qv Strict (inter_on_on lu lv)
| Ord.Lt -> inter_on_off lu v
| Ord.Gt -> smaller_lt_bound_on qv qu lu; OffEnd qv bv (inter_on_on u lv)
end
| (OnEnd qv bv lv) as v, (OffSin qu lu) as u ->
match Q.compare qu qv with
| Ord.Eq ->
match bv with
| Large -> OffSin qv (inter_off_off lu lv)
| Strict -> inter_off_off lu lv
end
| Ord.Lt -> smaller_lt_bound_off qu qv lv; OffSin qu (inter_on_off v lu)
| Ord.Gt -> inter_off_off u lv
end
end
with inter_off_off (u:off) (v:off) : off
requires { ordered_off u}
requires { ordered_off v }
ensures { ordered_off result }
ensures {
forall x:real. (mem_off x u /\ mem_off x v) <-> mem_off x result
}
ensures {
forall q.
(lt_bound_off q u) -> (lt_bound_off q v) ->
(lt_bound_off q result )
}
variant { length_off u + length_off v } =
match u, v with
| _, OffInf | OffInf, _ -> OffInf
| OffSin qu lu, OffSin qv lv ->
match Q.compare qu qv with
| Ord.Eq -> OffSin qu (inter_off_off lu lv)
| Ord.Lt -> inter_off_off lu v
| Ord.Gt -> inter_off_off u lv
end
| OffEnd qu bu lu, OffEnd qv bv lv ->
match Q.compare qu qv with
| Ord.Eq ->
let b = match bu, bv with
| Large, Large -> Large
| _ -> Strict
end
in
OffEnd qu b (inter_on_on lu lv)
| Ord.Lt -> inter_on_off lu v
| Ord.Gt -> inter_on_off lv u
end
| (OffSin qu lu) as u, (OffEnd qv bv lv) as v
| (OffEnd qv bv lv) as v, (OffSin qu lu) as u ->
match Q.compare qu qv with
| Ord.Eq -> match bv with
| Large -> OffSin qv (inter_on_off lv lu)
| Strict -> inter_on_off lv lu
end
| Ord.Lt -> inter_off_off lu v
| Ord.Gt -> inter_on_off lv u
end
end
in
let mk_off_option (l:off) : option t'
requires { ordered_off l }
ensures {
forall x:real. mem_off x l <->
match result with
| None -> false
| Some w -> mem x w.a
end
}
=
match l with
| OffInf -> None
| l -> Some { a = Off l }
end
in
match u.a,v.a with
| On u, On v -> Some { a = On (inter_on_on u v) }
| On u, Off v | Off v, On u -> mk_off_option (inter_on_off u v)
| Off u, Off v -> mk_off_option (inter_off_off u v)
end
(*
let inter (u:t') (v:t') : option t' let inter (u:t') (v:t') : option t'
ensures { ensures {
forall x:real. (mem x u.a /\ mem x v.a) <-> forall x:real. (mem x u.a /\ mem x v.a) <->
...@@ -428,7 +673,7 @@ module Union ...@@ -428,7 +673,7 @@ module Union
| Ord.Gt -> aux_option lu lv | Ord.Gt -> aux_option lu lv
end end
end end
*)
end end
src_common/union/why3session.xml
+ 1202
− 993
View file @ af9218d5
This diff is collapsed.
src_common/union__Union.ml
+ 150
− 162
View file @ af9218d5
type t0 = type on =
| Singleton of (Q.t) * t0 | OnSin of (Q.t) * on
| Inter of (Q.t) * Interval__Bound.t * (Q.t) * Interval__Bound.t * t0 | OnEnd of (Q.t) * Interval__Bound.t * off
| FiniteInf of (Q.t) * Interval__Bound.t | OnInf
| End and off =
| OffSin of (Q.t) * off
| OffEnd of (Q.t) * Interval__Bound.t * on
| OffInf
type t = type t =
| InfFinite of (Q.t) * Interval__Bound.t * t0 | On of on
| Finite of t0 | Off of off
| Inf
type t' = t type t' = t
let singleton (q: Q.t) : t' = Finite (Singleton (q, End)) let singleton (q: Q.t) : t' = Off (OffSin (q, OffInf))
let is_singleton (u: t') : (Q.t) option = let is_singleton (u: t') : (Q.t) option =
match u with match u with
| Inf -> None | Off OffSin (q, OffInf) -> Some q
| InfFinite (q, _, _) -> None | Off OffSin (q, OffSin (q', _)) -> None
| Finite Singleton (q, End) -> Some q | Off OffSin (_,
| Finite End -> assert false (* absurd *) OffEnd (q,
| Finite Inter (q, _, q', _, _) -> None _,
| Finite FiniteInf (q, _) -> None on)) ->
| Finite Singleton (q, Singleton (q', _)) -> None begin match on with
| Finite Singleton (_, Inter (q, _, q', _, _)) -> None | OnSin (q', _) -> None
| Finite Singleton (_, FiniteInf (q, _)) -> None | OnEnd (q', _, _) -> None
| OnInf -> None
end
| Off OffEnd (q,
_,
on) ->
begin match on with
| OnSin (q', _) -> None
| OnEnd (q', _, _) -> None
| OnInf -> None
end
| On OnSin (q, _) -> None
| On OnEnd (q, _, _) -> None
| On OnInf -> None
| Off OffInf -> assert false (* absurd *)
let min_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t) let min_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
(b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t = (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
...@@ -70,168 +86,140 @@ let max_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t) ...@@ -70,168 +86,140 @@ let max_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
| (Ord.Gt, _, _) -> (v1, b1) | (Ord.Gt, _, _) -> (v1, b1)
let inter (u: t') (v: t') : t' option = let inter (u: t') (v: t') : t' option =
let rec aux (u1: t0) (v1: t0) : t0 = let rec inter_on_on (u1: on) (v1: on) : on =
match (u1, v1) with match (u1, v1) with
| ((End, _) | (_, End)) -> End | ((u2, OnInf) | (OnInf, u2)) -> u2
| (Singleton (qu, | (OnSin (qu,
lu), lu),
Singleton (qv, OnSin (qv,
lv)) -> lv)) ->
begin match (Q_extra.compare qu qv) with begin match (Q_extra.compare qu qv) with
| Ord.Eq -> Singleton (qu, aux lu lv) | Ord.Eq -> OnSin (qu, inter_on_on lu lv)
| Ord.Lt -> aux lu v1 | Ord.Lt -> OnSin (qu, inter_on_on lu v1)
| Ord.Gt -> aux u1 lv | Ord.Gt -> OnSin (qv, inter_on_on u1 lv)
end end
| (FiniteInf (q, | (OnEnd (qu,
b), bu,
FiniteInf (q', lu),
b')) -> OnEnd (qv,
(let (q'', b'') = max_bound_inf q b q' b' in FiniteInf (q'', b'')) bv,
| (((Singleton (qu, lu) as u2), lv)) ->
(FiniteInf (qv, bv) as v2)) | ((FiniteInf (qv, bv) as v2),
(Singleton (qu, lu) as u2))) ->
begin match (Q_extra.compare qu qv) with begin match (Q_extra.compare qu qv) with
| Ord.Lt -> aux lu v2
| Ord.Gt -> u2
| Ord.Eq -> | Ord.Eq ->
begin match bv with (let b =
| Interval__Bound.Large -> u2 match (bu, bv) with
| Interval__Bound.Strict -> lu | (Interval__Bound.Large,
end Interval__Bound.Large) ->
Interval__Bound.Large
| _ -> Interval__Bound.Strict in
OnEnd (qu, b, inter_off_off lu lv))
| Ord.Lt -> OnEnd (qu, bu, inter_on_off v1 lu)
| Ord.Gt -> OnEnd (qv, bv, inter_on_off u1 lv)
end end
| (((FiniteInf (q, b) as u3), | (((OnSin (qu, lu) as u2),
(Inter (qv0, bv0, qv1, bv1, lv) as v3)) | ((Inter (qv0, bv0, qv1, bv1, (OnEnd (qv, bv, lv) as v2)) | ((OnEnd (qv, bv, lv) as v2),
lv) as v3), (OnSin (qu, lu) as u2))) ->
(FiniteInf (q, b) as u3))) -> begin match (Q_extra.compare qu qv) with
begin match (Q_extra.compare q qv0) with | Ord.Eq -> OnEnd (qv, Interval__Bound.Strict, inter_on_off lu lv)
| Ord.Lt -> v3 | Ord.Lt -> OnSin (qu, inter_on_on lu v2)
| Ord.Gt -> | Ord.Gt -> OnEnd (qv, bv, inter_on_off u2 lv)
begin match (Q_extra.compare q qv1) with end
| Ord.Lt -> Inter (q, b, qv1, bv1, lv) and inter_on_off (u3: on) (v3: off) : off =
| Ord.Gt -> aux u3 lv match (u3, v3) with
| Ord.Eq -> | (_, OffInf) -> OffInf
begin match (b, bv1) with | (OnInf, u4) -> u4
| (Interval__Bound.Large, | (OnSin (qu,
Interval__Bound.Large) -> lu),
Singleton (q, lv) OffSin (qv,
| _ -> lv lv)) ->
end begin match (Q_extra.compare qu qv) with
end | Ord.Eq -> inter_on_off lu lv
| Ord.Lt -> inter_on_off lu v3
| Ord.Gt -> OffSin (qv, inter_on_off u3 lv)
end
| (OnEnd (qu,
bu,
lu),
OffEnd (qv,
bv,
lv)) ->
begin match (Q_extra.compare qu qv) with
| Ord.Eq -> | Ord.Eq ->
begin match (b, bv0) with begin match (bu, bv) with
| (Interval__Bound.Strict, | (Interval__Bound.Large,
Interval__Bound.Large) -> Interval__Bound.Large) ->
Inter (qv0, b, qv1, bv1, lv) OffSin (qu, inter_on_off lv lu)
| _ -> v3 | _ -> inter_on_off lv lu
end end
| Ord.Lt -> inter_off_off lu v3
| Ord.Gt -> OffEnd (qv, bv, inter_on_on u3 lv)
end end
| (((Singleton (qu, lu) as u4), | ((OnSin (qu, lu) as u4),
(Inter (qv0, bv0, qv1, bv1, lv) as v4)) | ((Inter (qv0, bv0, qv1, bv1, (OffEnd (qv, bv, lv) as v4)) ->
lv) as v4), begin match (Q_extra.compare qu qv) with
(Singleton (qu, lu) as u4))) -> | Ord.Eq -> OffEnd (qv, Interval__Bound.Strict, inter_on_on lu lv)
begin match (Q_extra.compare qu qv0) with | Ord.Lt -> inter_on_off lu v4
| Ord.Lt -> aux lu v4 | Ord.Gt -> OffEnd (qv, bv, inter_on_on u4 lv)
| Ord.Gt -> end
begin match (Q_extra.compare qu qv1) with | ((OnEnd (qv, bv, lv) as v5),
| Ord.Lt -> Singleton (qu, aux lu v4) (OffSin (qu, lu) as u5)) ->
| Ord.Gt -> aux u4 lv begin match (Q_extra.compare qu qv) with
| Ord.Eq ->
begin match bv1 with
| Interval__Bound.Large -> Singleton (qu, aux lu lv)
| _ -> aux lu lv
end
end
| Ord.Eq -> | Ord.Eq ->
begin match bv0 with begin match bv with
| Interval__Bound.Large -> Singleton (qu, aux lu v4) | Interval__Bound.Large -> OffSin (qv, inter_off_off lu lv)
| _ -> aux lu v4 | Interval__Bound.Strict -> inter_off_off lu lv
end end
| Ord.Lt -> OffSin (qu, inter_on_off v5 lu)
| Ord.Gt -> inter_off_off u5 lv
end
and inter_off_off (u6: off) (v6: off) : off =
match (u6, v6) with
| ((_, OffInf) | (OffInf, _)) -> OffInf
| (OffSin (qu,
lu),
OffSin (qv,
lv)) ->
begin match (Q_extra.compare qu qv) with
| Ord.Eq -> OffSin (qu, inter_off_off lu lv)
| Ord.Lt -> inter_off_off lu v6
| Ord.Gt -> inter_off_off u6 lv
end end
| (Inter (qu0, | (OffEnd (qu,
bu0, bu,
qu1,
bu1,
lu), lu),
Inter (qv0, OffEnd (qv,
bv0, bv,
qv1,
bv1,
lv)) -> lv)) ->
(let v' = v1 in let u' = u1 in begin match (Q_extra.compare qu qv) with
let small_big (qu01: Q.t) (bu01: Interval__Bound.t) (qu11: Q.t) | Ord.Eq ->
(bu11: Interval__Bound.t) (lu1: t0) (u5: t0) (qv01: Q.t) (let b =
(bv01: Interval__Bound.t) (qv11: Q.t) match (bu, bv) with
(bv11: Interval__Bound.t) (lv1: t0) (v5: t0) : t0 =
match (Q_extra.compare qu11 qv01) with
| Ord.Eq ->
begin match (bu11, bv01) with
| (Interval__Bound.Large, | (Interval__Bound.Large,
Interval__Bound.Large) -> Interval__Bound.Large) ->
Singleton (qu11, aux lu1 v5) Interval__Bound.Large
| _ -> aux lu1 v5 | _ -> Interval__Bound.Strict in
end OffEnd (qu, b, inter_on_on lu lv))
| Ord.Lt -> aux lu1 v5 | Ord.Lt -> inter_on_off lu v6
| Ord.Gt -> | Ord.Gt -> inter_on_off lv u6
(let (qw0, bw0) = max_bound_inf qu01 bu01 qv01 bv01 in end
Inter (qw0, bw0, qu11, bu11, aux lu1 v5)) in | (((OffSin (qu, lu) as u7),
match (Q_extra.compare qu1 qv1) with (OffEnd (qv, bv, lv) as v7)) | ((OffEnd (qv, bv, lv) as v7),
| Ord.Eq -> (OffSin (qu, lu) as u7))) ->
(let (qw01, bw01) = max_bound_inf qu0 bu0 qv0 bv0 in begin match (Q_extra.compare qu qv) with
let b = | Ord.Eq ->
match (bu1, bv1) with begin match bv with
| (Interval__Bound.Large, | Interval__Bound.Large -> OffSin (qv, inter_on_off lv lu)
Interval__Bound.Large) -> | Interval__Bound.Strict -> inter_on_off lv lu
Interval__Bound.Large end
| _ -> Interval__Bound.Strict in | Ord.Lt -> inter_off_off lu v7
Inter (qw01, bw01, qv1, b, aux lu lv)) | Ord.Gt -> inter_on_off lv u7
| Ord.Lt -> small_big qu0 bu0 qu1 bu1 lu u1 qv0 bv0 qv1 bv1 lv v1 end in
| Ord.Gt -> small_big qv0 bv0 qv1 bv1 lv v1 qu0 bu0 qu1 bu1 lu u1) in let mk_off_option (l: off) : t' option =
let aux_option (lu: t0) (lv: t0) : t' option = match l with
match aux lu lv with | OffInf -> None
| End -> None | l1 -> Some (Off l1) in
| lw -> Some (Finite lw) in
match (u, v) with match (u, v) with
| (Inf, _) -> Some v | (On u8, On v8) -> Some (On (inter_on_on u8 v8))
| (_, Inf) -> Some u | ((On u8, Off v8) | (Off v8, On u8)) -> mk_off_option (inter_on_off u8 v8)
| (InfFinite (qu1, | (Off u8, Off v8) -> mk_off_option (inter_off_off u8 v8)
bu1,
lu),
InfFinite (qv1,
bv1,
lv)) ->
begin match (Q_extra.compare qu1 qv1) with
| Ord.Eq ->
(let b =
match (bu1, bv1) with
| (Interval__Bound.Large,
Interval__Bound.Large) ->
Interval__Bound.Large
| _ -> Interval__Bound.Strict in
Some (InfFinite (qu1, b, aux lu lv)))
| Ord.Lt ->
Some (InfFinite (qu1, bu1,
aux lu (Inter (qu1, Interval__Bound.Strict, qv1, bv1, lv))))
| Ord.Gt ->
Some (InfFinite (qv1, bv1,
aux (Inter (qv1, Interval__Bound.Strict, qu1, bu1, lu)) lv))
end
| (Finite lu, Finite lv) -> aux_option lu lv
| ((Finite lu, InfFinite (qv1, bv1, lv)) | (InfFinite (qv1, bv1, lv),
Finite lu)) ->
(let (qu0, bu0) =
match lu with
| End -> assert false (* absurd *)
| Singleton (qu01, _) -> (qu01, Interval__Bound.Large)
| Inter (qu01, bu01, _, _, _) -> (qu01, bu01)
| FiniteInf (qu01, bu01) -> (qu01, bu01) in
match (Q_extra.compare qu0 qv1) with
| Ord.Eq ->
begin match (bu0, bv1) with
| (Interval__Bound.Large,
Interval__Bound.Large) ->
aux_option lu (Singleton (qv1, lv))
| _ -> aux_option lu lv
end
| Ord.Lt -> aux_option lu (Inter (qu0, bu0, qv1, bv1, lv))
| Ord.Gt -> aux_option lu lv)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment