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

[Solver] cleanup: remove ClSem unused

parent 7f413fda
No related branches found
No related tags found
No related merge requests found
...@@ -380,93 +380,6 @@ let print_dem_runable (type k) (type d) (k : (k,d) dem) fmt s = ...@@ -380,93 +380,6 @@ let print_dem_runable (type k) (type d) (k : (k,d) dem) fmt s =
let () = Print.pdem_runable.Print.pdem_runable <- print_dem_runable let () = Print.pdem_runable.Print.pdem_runable <- print_dem_runable
module ClSem : sig
include Datatype
val cl: Cl.t -> t
val sem: 'a sem -> 'a -> t
type view =
| Cl: Cl.t -> view
| Sem: 'a sem * 'a -> view
val view: t -> view
val is_cl: t -> bool
val is_sem: t -> bool
end
= struct
type view = Def.clsem =
| Cl: Cl.t -> view
| Sem: 'a sem * 'a -> view
let cl cl = Cl cl
let sem sem v = Sem(sem,v)
let is_cl t = match t with Cl _ -> true | Sem _ -> false
let is_sem t = match t with Cl _ -> false | Sem _ -> true
let view t = t
include MkDatatype(struct
type t = view
let equal t1 t2 =
match t1,t2 with
| Cl _, Sem _ | Sem _, Cl _ -> false
| Cl cl1, Cl cl2 -> Cl.equal cl1 cl2
| Sem (sem1,v1), Sem (sem2,v2) ->
match Sem.Eq.eq_type sem1 sem2 with
| None -> false
| Some Eqtype.Eq ->
let module Sem = (val get_sem sem1) in
Sem.equal v1 v2
let compare t1 t2 =
match t1,t2 with
| Cl _, Sem _ -> 1
| Sem _, Cl _ -> -1
| Cl cl1, Cl cl2 -> Cl.compare cl1 cl2
| Sem (sem1,v1), Sem (sem2,v2) ->
match Sem.Eq.eq_type sem1 sem2 with
| None -> Sem.compare sem1 sem2
| Some Eqtype.Eq ->
let module Sem = (val get_sem sem1) in
Sem.compare v1 v2
let hash t =
match t with
| Cl cl -> Cl.hash cl
| Sem(sem,v) ->
let module S = (val get_sem sem) in
Hashcons.combine (Sem.hash sem)
(S.hash v)
let print fmt t =
match t with
| Cl cl -> Cl.print fmt cl
| Sem (sem,v) ->
let module S = (val get_sem sem) in
Format.fprintf fmt "%a:%a"
Sem.print sem S.print v
end)
(* let cl (x:Cl.t) : t = Obj.magic ((x:> int) : int) *)
(* let sem (type a) (sem: a sem) (v:a) : t = Obj.magic (Sem(sem,v) : view) *)
(* let is_cl (t:t) = Obj.is_int (Obj.repr t) *)
(* let is_sem (t:t) = not (Obj.is_int (Obj.repr t)) *)
(* let view (t:t) : view = *)
(* if is_cl t then Cl (Obj.magic t : Cl.t) *)
(* else (Obj.magic t : view) *)
(* let equal x y = *)
(* x == y || (is_sem x && is_sem y && *)
(* let x = Obj.repr x in *)
(* let y = Obj.repr y in *)
(* let sem = *)
end
(** {2 Dom Sem continued} *) (** {2 Dom Sem continued} *)
module type DomTable = DomTable' with type delayed = delayed_t module type DomTable = DomTable' with type delayed = delayed_t
......
...@@ -26,22 +26,6 @@ open Types ...@@ -26,22 +26,6 @@ open Types
exception NotNormalized exception NotNormalized
module ClSem : sig
include Datatype
val cl: Cl.t -> t
val sem: 'a sem -> 'a -> t
type view =
| Cl: Cl.t -> view
| Sem: 'a sem * 'a -> view
val view: t -> view
val is_cl: t -> bool
val is_sem: t -> bool
end
type exp_same_sem = type exp_same_sem =
| ExpSameSem : pexp * Cl.t * Cl.t * 'a sem * 'a -> exp_same_sem | ExpSameSem : pexp * Cl.t * Cl.t * 'a sem * 'a -> exp_same_sem
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment