diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f7d2b8c8848129fe69798006dc5ce09568315c84..ceec9c6f463902c5b16cd574f6e78466eb0505d0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -3,6 +3,7 @@ Tests:
- eval `opam config env`
- make
- make tests
- tags:
+ - make api
+ tags:
except:
- tags
diff --git a/Makefile b/Makefile
index 09c57f9dd06225106c4e7f771fa8e377c5698242..eb862453fff7200a1ee4e522e65d94ac04cd603b 100644
--- a/Makefile
+++ b/Makefile
@@ -2,7 +2,7 @@
PACKAGES=oUnit zarith ocamlgraph cryptokit #-package lablgtk2
# I don't understand warning 18
-OPTIONS=-tag annot -no-sanitize -tag debug -use-ocamlfind -cflags -w,+a-4-9-18-41-44-40-45-42 -cflags -warn-error,+5+10+8+12+20+11 -tag strict_sequence -cflag -bin-annot -j 8
+OPTIONS=-tag annot -no-sanitize -tag debug -use-ocamlfind -cflags -w,+a-4-9-18-41-44-40-45-42-50 -cflags -warn-error,+5+10+8+12+20+11 -tag strict_sequence -cflag -bin-annot -j 8
#OPTIONS += -cflags -warn-error,+a
DIRECTORIES=src src/util src/inputlang/altergo src/inputlang/dimacs_cnf src/inputlang/smtlib2 tests src/cmd src/arith fuzz
OCAMLBUILD=ocamlbuild \
diff --git a/api.odocl b/api.odocl
index 959afdf27b9899bcb792020a3f7f7fe5a2d94d4f..c1dc4b64ae382a6f5272d9b6d8e5f4cf7b169f1d 100644
--- a/api.odocl
+++ b/api.odocl
@@ -11,8 +11,6 @@ Scheduler
Bool
Equality
Dimacs
-Why_typing
-Ty
Why_ptree
Why_lexer
Why_parser
@@ -32,10 +30,8 @@ Simple_vector
Number
Exthtbl
Strings
-Eqtype
Weakhtbl
Pp
-Rc
Loc
IArray
Debug
diff --git a/src/arith/arith.ml b/src/arith/arith.ml
index 452866b13ee6a09e9ab532f9d75df085000b1361..472ee869a5abe1a99492a0a622dccfda09a7e867 100644
--- a/src/arith/arith.ml
+++ b/src/arith/arith.ml
@@ -862,7 +862,7 @@ module ConPoly = struct
let p2 =
match Sem.Eq.eq_type sem sem' with
| None -> raise Impossible (* understand why that happend *)
- | Some Eqtype.Eq ->
+ | Some Types.Eq ->
let p2 = x_p_cy (monome Q.one cl2) Q.minus_one v in
{imp = p2; exp = p2}
in
@@ -1090,7 +1090,7 @@ module ExpMulSubst = struct
let return () : a Conflict.rescon =
match Explanation.Con.Eq.eq_type confact con with
| None -> GOther (confact,())
- | Some Eqtype.Eq -> GRequested () in
+ | Some Types.Eq -> GRequested () in
begin match exp with
| Mul(f,g) as v ->
GenEquality.equality t age f (get_repr_at t age f);
diff --git a/src/bool.ml b/src/bool.ml
index f0274945ca723c97e93e7a3d5b05f71ef7725b32..68681a47c78c23e934a896cbafafc8cbaff02c54 100644
--- a/src/bool.ml
+++ b/src/bool.ml
@@ -496,7 +496,7 @@ module ChoBool = struct
let return (s:bool Types.Cl.M.t) : a rescon =
match Explanation.Con.Eq.eq_type conclause con with
| None -> GOther (conclause,s)
- | Some Eqtype.Eq -> GRequested s in
+ | Some Types.Eq -> GRequested s in
ComputeConflict.set_dec_cho t chobool cl;
return (Cl.M.singleton cl b)
@@ -612,7 +612,7 @@ module ExpMerge = struct
let return (s:bool Types.Cl.M.t) : a Conflict.rescon =
match Explanation.Con.Eq.eq_type conclause con with
| None -> GOther (conclause,s)
- | Some Eqtype.Eq -> GRequested s in
+ | Some Types.Eq -> GRequested s in
match exp with
| Merge (pexp,cl1,cl2) ->
let s = Cl.M.empty in
@@ -843,7 +843,7 @@ module ConClause = struct
(* then GRequested Cl.M.empty *)
(* else *)
(* match Dom.Eq.coerce_type dom dom' with *)
- (* | Eqtype.Eq -> *)
+ (* | Types.Eq -> *)
(* if Cl.equal cl cl_true || Cl.equal cl cl_false then *)
(* GRequested Cl.M.empty *)
(* else *)
@@ -851,3 +851,5 @@ module ConClause = struct
end
module EC = Conflict.RegisterCon(ConClause)
+
+
diff --git a/src/conflict.ml b/src/conflict.ml
index 1e44a46565eec81d8b2d43611de8ab79009acaba..d16d0ce2d081d0dd2a9dbbad4bd0ea0e15fbf53b 100644
--- a/src/conflict.ml
+++ b/src/conflict.ml
@@ -40,7 +40,7 @@ type 'a rescon = 'a Explanation.rescon =
let return : type a b. a con -> b con -> b -> a rescon = fun con con' v ->
match Explanation.Con.Eq.eq_type con con' with
- | Some Eqtype.Eq -> GRequested v
+ | Some Types.Eq -> GRequested v
| None -> GOther(con',v)
type explearnt =
@@ -187,7 +187,7 @@ let return_rescon (type a) (type b) (con : a con) (x:a)
(conrequested : b con) : b rescon =
match Con.Eq.eq_type con conrequested with
| None -> (GOther (con,x) : b rescon)
- | Some Eqtype.Eq -> GRequested x
+ | Some Types.Eq -> GRequested x
let mk_confact con = return_rescon confact () con
@@ -382,7 +382,7 @@ let explimit : explimit exp = Exp.create_key "Conflict.explimit"
let is_explimit (Pexp(_,exp,k,_,_)) =
match Exp.Eq.eq_type explimit exp with
- | Some Eqtype.Eq -> Some (k : explimit)
+ | Some Types.Eq -> Some (k : explimit)
| None -> None
@@ -643,7 +643,7 @@ module ComputeConflict = struct
(* let Pexp(age,k,exp,_,_) = pexp in
match Exp.Eq.eq_type k expdirect with
| None -> get_pexp_aux t pexp con
- | Some Eqtype.Eq ->
+ | Some Types.Eq ->
match exp with
| DirectDom(dom,cl) ->
match get_dom t age cl dom with
@@ -1243,7 +1243,7 @@ let () =
equal_chogen :=
(fun (Explanation.GCho(cho1,k1)) (Explanation.GCho(cho2,k2)) ->
match Cho.Eq.eq_type cho1 cho2 with
- | Some (Eqtype.Eq, Eqtype.Eq) ->
+ | Some (Types.Eq, Types.Eq) ->
let module C = (val get_cho cho1) in
C.Key.equal k1 k2
| None -> false
diff --git a/src/equality.ml b/src/equality.ml
index 249ac1e867f5717d8be5e4842c21bbea5984d85b..9b2216325ea1d6f9f24db3527d8b89773bf061b4 100644
--- a/src/equality.ml
+++ b/src/equality.ml
@@ -713,7 +713,7 @@ module ConDis = struct
Explanation.Age.t -> a dom -> Cl.t -> a option -> t rescon =
fun t age dom' cl dis ->
match Dom.Eq.coerce_type dom' dom with
- | Eqtype.Eq ->
+ | Types.Eq ->
if ComputeConflict.before_first_dec t age
then
let v = Hideable cl, Explanation.Deps.empty in
@@ -894,7 +894,7 @@ module ExpSubst = struct
fun t age con exp ->
let return_dis (con : a con) i : a Conflict.rescon =
match Explanation.Con.Eq.coerce_type con ConDis.key with
- | Eqtype.Eq ->
+ | Types.Eq ->
GRequested (DInt.M.singleton i
(ConDis.Unknown, Explanation.Deps.empty))
in
@@ -954,7 +954,7 @@ module ExpSubst = struct
fun t age dom' cl con exp ->
let return_dis (con : a con) i : a Conflict.rescon =
match Explanation.Con.Eq.coerce_type con ConDis.key with
- | Eqtype.Eq ->
+ | Types.Eq ->
GRequested (DInt.M.singleton i
((if ComputeConflict.before_first_dec t age
then ConDis.Hideable cl
diff --git a/src/solver.ml b/src/solver.ml
index 38c2a167aeef6c331220c32081ea74daeb0b6ae5..78d08954bfc454b2fde07a68cac4423ac3ed305d 100644
--- a/src/solver.ml
+++ b/src/solver.ml
@@ -642,7 +642,7 @@ module Delayed = struct
~map:(function
| Events.Wait.Event(dem',event) ->
match Dem.Eq.coerce_type dem dem' with
- | Eqtype.Eq, Eqtype.Eq -> (event:k)
+ | Types.Eq, Types.Eq -> (event:k)
)
(Cl.M.find_def [] cl d.env.event_propa)
@@ -656,7 +656,7 @@ module Delayed = struct
~map:(function
| Events.Wait.Event(dem',event) ->
match Dem.Eq.coerce_type dem dem' with
- | Eqtype.Eq, Eqtype.Eq -> (event:k)
+ | Types.Eq, Types.Eq -> (event:k)
)
(Cl.M.find_def Bag.empty cl d.env.event)
diff --git a/src/solver.mli b/src/solver.mli
index 311a2652cc7bb47c0626384cf450ecbdd8bed006..063a9b940f201bd585b5185e8903940e425186e6 100644
--- a/src/solver.mli
+++ b/src/solver.mli
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-open Stdlib
open Explanation
open Types
diff --git a/src/types.ml b/src/types.ml
index 082819b7459501a46a64a276cc076a2262efe3b0..45b33105dc8496467c82393ebc9259cf09c11d83 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -70,6 +70,10 @@ module Ty = struct
end
+exception BadCoercion
+
+type (_,_) eq = Eq : ('a,'a) eq
+
module type Key = sig
module K: Datatype
@@ -84,7 +88,16 @@ module type Key = sig
val iter : iter -> unit
val hint_size : unit -> int
- module Eq: Eqtype.S1 with type 'a t = 'a k
+ module Eq: sig
+ val eq_type : 'a k -> 'b k -> ('a,'b) eq option
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned *)
+
+ val coerce_type : 'a k -> 'b k -> ('a,'b) eq
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned otherwise
+ the exception BadCoercion is raised *)
+ end
val create_key: string -> 'a k
module MkVector(D:sig type ('a,'b) t end)
@@ -114,8 +127,24 @@ module Make_key(X:sig end): Key = struct
let iter f = K.iter f.iter
let hint_size = K.hint_size
- module Eq = Eqtype.Make1(struct type 'a t = 'a k end)
let create_key s = K.create s
+
+ (** the 'a k can be used as equality witness because K gives fresh values *)
+ module Eq = struct
+ let eq_type :
+ type a b. a k -> b k -> (a,b) eq option =
+ fun a b ->
+ if equal a b
+ then Some ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
+ else None
+
+ let coerce_type :
+ type a b. a k -> b k -> (a,b) eq =
+ fun a b ->
+ if equal a b
+ then ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
+ else raise BadCoercion
+ end
module MkVector(D:sig type ('a,'b) t end) =
Vector_hetero.Make1(struct type 'a t = 'a k end)(D)
module MkMap(D:sig type ('a,'b) t end) =
@@ -258,14 +287,14 @@ module RegisterSem (D:Sem) = struct
| Sem(_,tya,sema,va), Sem(_,tyb,semb,vb) ->
match Sem.Eq.coerce_type sema D.key,
Sem.Eq.coerce_type semb D.key with
- | Eqtype.Eq, Eqtype.Eq ->
+ | Eq, Eq ->
Ty.equal tya tyb && D.equal va vb
let hash: t -> int = fun a ->
match a with
| Sem(_,tya,sema,va) ->
match Sem.Eq.coerce_type sema D.key with
- | Eqtype.Eq ->
+ | Eq ->
Hashcons.combine (Ty.hash tya) (D.hash va)
let set_tag: int -> t -> t = fun tag x ->
@@ -307,7 +336,7 @@ module RegisterSem (D:Sem) = struct
let sem : t -> D.t = function
| Cl.Sem(_,_,sem,v) ->
match Sem.Eq.coerce_type sem D.key with
- | Eqtype.Eq -> v
+ | Eq -> v
let ty = ClSem.ty
@@ -344,8 +373,20 @@ module type Key2 = sig
type iter = {iter : 'k 'd. ('k,'d) k -> unit}
val iter : iter -> unit
- module Eq: Eqtype.S2 with type ('k,'d) t = ('k,'d) k
val create_key: string -> ('k,'d) k
+
+ module Eq: sig
+ val eq_type : ('a1,'b1) k -> ('a2,'b2) k
+ -> (('a1,'a2) eq * ('b1,'b2) eq) option
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned *)
+
+ val coerce_type : ('a1,'b1) k -> ('a2,'b2) k
+ -> ('a1,'a2) eq * ('b1,'b2) eq
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned otherwise
+ the exception BadCoercion is raised *)
+ end
module MkVector(D:sig type ('k,'d,'b) t end)
: Vector_hetero.S2 with type ('k,'d) key = ('k,'d) k
and type ('k,'d,'b) data = ('k,'d,'b) D.t
@@ -362,8 +403,33 @@ module Make_key2(X:sig end) = struct
type iter = {iter : 'k 'd. ('k,'d) k -> unit}
let iter f = K.iter f.iter
- module Eq = Eqtype.Make2(struct type ('a,'b) t = ('a,'b) k end)
let create_key s = K.create s
+
+ (** the ('k,'d) k can be used as equality witness because K gives
+ fresh values *)
+ module Eq = struct
+
+ let eq_type :
+ type a1 b1 a2 b2. (a1,b1) k -> (a2,b2) k
+ -> ((a1,a2) eq * (b1,b2) eq) option =
+ fun a b ->
+ if equal a b
+ then let eq1 = (Obj.magic (Eq : (a1,a1) eq) : (a1,a2) eq) in
+ let eq2 = (Obj.magic (Eq : (b1,b1) eq) : (b1,b2) eq) in
+ Some (eq1,eq2)
+ else None
+
+ let coerce_type :
+ type a1 b1 a2 b2. (a1,b1) k -> (a2,b2) k
+ -> ((a1,a2) eq * (b1,b2) eq) =
+ fun a b ->
+ if equal a b
+ then let eq1 = (Obj.magic (Eq : (a1,a1) eq) : (a1,a2) eq) in
+ let eq2 = (Obj.magic (Eq : (b1,b1) eq) : (b1,b2) eq) in
+ (eq1,eq2)
+ else raise BadCoercion
+
+ end
module MkVector(D:sig type ('k,'d,'b) t end) =
Vector_hetero.Make2(struct type ('k,'d) t = ('k,'d) k end)(D)
end
diff --git a/src/types.mli b/src/types.mli
index 1810b09b949c341c275398920399bda654185512..1df409b922d74635a03b067b4f9dfafe8a5d0b55 100644
--- a/src/types.mli
+++ b/src/types.mli
@@ -54,6 +54,10 @@ end
exception UnregisteredKey
exception AlreadyRegisteredKey
+
+exception BadCoercion
+type (_,_) eq = Eq : ('a,'a) eq
+
module type Key = sig
module K: Datatype
@@ -69,7 +73,16 @@ module type Key = sig
val iter : iter -> unit
val hint_size : unit -> int
- module Eq: Eqtype.S1 with type 'a t = 'a k
+ module Eq: sig
+ val eq_type : 'a k -> 'b k -> ('a,'b) eq option
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned *)
+
+ val coerce_type : 'a k -> 'b k -> ('a,'b) eq
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned otherwise
+ the exception BadCoercion is raised *)
+ end
val create_key: string -> 'a k
module MkVector(D:sig type ('a,'b) t end)
@@ -171,8 +184,20 @@ module type Key2 = sig
type iter = {iter : 'k 'd. ('k,'d) k -> unit}
val iter : iter -> unit
- module Eq: Eqtype.S2 with type ('k,'d) t = ('k,'d) k
val create_key: string -> ('k,'d) k
+
+ module Eq: sig
+ val eq_type : ('a1,'b1) k -> ('a2,'b2) k
+ -> (('a1,'a2) eq * ('b1,'b2) eq) option
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned *)
+
+ val coerce_type : ('a1,'b1) k -> ('a2,'b2) k
+ -> ('a1,'a2) eq * ('b1,'b2) eq
+ (** If the two arguments are physically identical then an equality witness
+ between the types is returned otherwise
+ the exception BadCoercion is raised *)
+ end
module MkVector(D:sig type ('k,'d,'b) t end)
: Vector_hetero.S2 with type ('k,'d) key = ('k,'d) k
and type ('k,'d,'b) data = ('k,'d,'b) D.t
diff --git a/src/util/eqtype.ml b/src/util/eqtype.ml
deleted file mode 100644
index d076cb837469b6eba62dbee1df34ba66ff2af797..0000000000000000000000000000000000000000
--- a/src/util/eqtype.ml
+++ /dev/null
@@ -1,103 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2013 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-exception BadCoercion
-
-type (_,_) eq = Eq : ('a,'a) eq
-
-module type S1 = sig
- type 'a t
-
- val eq_type : 'a t -> 'b t -> ('a,'b) eq option
- (** If the two arguments are physically identical then an equality witness
- between the types is returned *)
-
- val coerce_type : 'a t -> 'b t -> ('a,'b) eq
- (** If the two arguments are physically identical then an equality witness
- between the types is returned otherwise
- the exception BadCoercion is raised *)
-
-
-end
-
-module Make1(X : sig type 'a t end) =
-struct
- type 'a t = 'a X.t
-
- let eq_type :
- type a b. a X.t -> b X.t -> (a,b) eq option =
- fun a b ->
- if Obj.repr a == Obj.repr b
- then Some ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
- else None
-
- let coerce_type :
- type a b. a X.t -> b X.t -> (a,b) eq =
- fun a b ->
- if Obj.repr a == Obj.repr b
- then ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
- else raise BadCoercion
-
-end
-
-module type S2 = sig
- type ('a,'b) t
-
- val eq_type : ('a1,'b1) t -> ('a2,'b2) t
- -> (('a1,'a2) eq * ('b1,'b2) eq) option
- (** If the two arguments are physically identical then an equality witness
- between the types is returned *)
-
- val coerce_type : ('a1,'b1) t -> ('a2,'b2) t
- -> ('a1,'a2) eq * ('b1,'b2) eq
- (** If the two arguments are physically identical then an equality witness
- between the types is returned otherwise
- the exception BadCoercion is raised *)
-
-
-end
-
-module Make2(X : sig type ('a,'b) t end) =
-struct
- type ('a,'b) t = ('a,'b) X.t
-
- let eq_type :
- type a1 b1 a2 b2. (a1,b1) X.t -> (a2,b2) X.t
- -> ((a1,a2) eq * (b1,b2) eq) option =
- fun a b ->
- if Obj.repr a == Obj.repr b
- then let eq1 = (Obj.magic (Eq : (a1,a1) eq) : (a1,a2) eq) in
- let eq2 = (Obj.magic (Eq : (b1,b1) eq) : (b1,b2) eq) in
- Some (eq1,eq2)
- else None
-
- let coerce_type :
- type a1 b1 a2 b2. (a1,b1) X.t -> (a2,b2) X.t
- -> ((a1,a2) eq * (b1,b2) eq) =
- fun a b ->
- if Obj.repr a == Obj.repr b
- then let eq1 = (Obj.magic (Eq : (a1,a1) eq) : (a1,a2) eq) in
- let eq2 = (Obj.magic (Eq : (b1,b1) eq) : (b1,b2) eq) in
- (eq1,eq2)
- else raise BadCoercion
-
-end
diff --git a/src/util/eqtype.mli b/src/util/eqtype.mli
deleted file mode 100644
index 8ee5be45862e93874c7286ca0c6a5254f7c0596f..0000000000000000000000000000000000000000
--- a/src/util/eqtype.mli
+++ /dev/null
@@ -1,62 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2013 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-exception BadCoercion
-
-type (_,_) eq = Eq : ('a,'a) eq
-
-module type S1 = sig
- type 'a t
-
- val eq_type : 'a t -> 'b t -> ('a,'b) eq option
- (** If the two arguments are physically identical then an equality witness
- between the types is returned *)
-
- val coerce_type : 'a t -> 'b t -> ('a,'b) eq
- (** If the two arguments are physically identical then an equality witness
- between the types is returned otherwise
- the exception BadCoercion is raised *)
-
-
-end
-
-module Make1(X : sig type 'a t end) : S1 with type 'a t = 'a X.t
-
-module type S2 = sig
- type ('a,'b) t
-
- val eq_type : ('a1,'b1) t -> ('a2,'b2) t
- -> (('a1,'a2) eq * ('b1,'b2) eq) option
- (** If the two arguments are physically identical then an equality witness
- between the types is returned *)
-
- val coerce_type : ('a1,'b1) t -> ('a2,'b2) t
- -> ('a1,'a2) eq * ('b1,'b2) eq
- (** If the two arguments are physically identical then an equality witness
- between the types is returned otherwise
- the exception BadCoercion is raised *)
-
-
-end
-
-
-module Make2(X : sig type ('a,'b) t end) : S2 with type ('a,'b) t = ('a,'b) X.t