[sledge] Cleanup of Import

Summary:
Work on the containers revealed that 1b8746d21 was premature, and this
diff is in part a revert of that. The objectives for the global
namespace are:

- self-consistent as much as possible
- rich data type operations
- does not require maintaining lots of tedious library wrapping code
- has Marshalable containers
- has containers with functorial interfaces

For these aims, it's best to stick with Core. Base isn't enough to
define functorial interfaces for collections (without a lot of tedious
wrapping code to keep in sync manually), and since a few modules not
in Core_kernel are needed anyhow.

Reviewed By: ngorogiannis

Differential Revision: D20583756

fbshipit-source-id: d939be7d0
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 7ab19955bb
commit fe62eeadab

@ -11,11 +11,11 @@ let config_file_env_var = "SLEDGE_CONFIG"
let exe_relative_config_file_path = "config"
let config_file =
match Core.Sys.getenv config_file_env_var with
match Sys.getenv config_file_env_var with
| Some file -> file
| None ->
Filename.concat
(Filename.dirname Caml.Sys.executable_name)
(Filename.dirname Sys.executable_name)
exe_relative_config_file_path
let contents =

@ -45,7 +45,7 @@ let pp fs =
in
bindings >> Array.pp "@," (pp_pair Var.print Interval.print) fs
let report_fmt_thunk = Fun.flip pp
let report_fmt_thunk = Fn.flip pp
let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||])
let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string
let apron_var_of_reg = Reg.name >> apron_var_of_name
@ -134,8 +134,8 @@ and apron_texpr_of_llair_term tm q typ =
| Div -> Some (mk_arith_binop typ Texpr0.Div)
| Eq -> Some (mk_bool_binop typ q Tcons0.EQ)
| Dq -> Some (mk_bool_binop typ q Tcons0.DISEQ)
| Lt -> Some (Fun.flip (mk_bool_binop typ q Tcons0.SUP))
| Le -> Some (Fun.flip (mk_bool_binop typ q Tcons0.SUPEQ))
| Lt -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUP))
| Le -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUPEQ))
| _ -> None
in
let* te1 = apron_texpr_of_llair_term t1 q typ in

@ -354,7 +354,7 @@ module Llvalue = struct
let sexp_of_t llv = Sexp.Atom (Llvm.string_of_llvalue llv)
end
let struct_rec = Exp.struct_rec (module Llvalue)
let struct_rec = Staged.unstage (Exp.struct_rec (module Llvalue))
let ptr_fld x ~ptr ~fld ~lltyp =
let offset =

@ -7,9 +7,8 @@
(** SLEdge command line interface *)
let () = Printexc.record_backtrace Version.debug
let () = Backtrace.Exn.set_recording Version.debug
module Command = Core.Command
open Command.Let_syntax
type 'a param = 'a Command.Param.t
@ -47,7 +46,7 @@ let command ~summary ?readme param =
Format.printf "@\nRESULT: Success: Invalid Accesses: %i@."
(Report.invalid_access_count ())
with exn ->
let bt = Caml.Printexc.get_raw_backtrace () in
let bt = Printexc.get_raw_backtrace () in
Trace.flush () ;
( match exn with
| Frontend.Invalid_llvm msg ->
@ -57,8 +56,8 @@ let command ~summary ?readme param =
| Failure msg -> Format.printf "@\nRESULT: Internal error: %s@." msg
| _ ->
Format.printf "@\nRESULT: Unknown error: %s@."
(Caml.Printexc.to_string exn) ) ;
Caml.Printexc.raise_with_backtrace exn bt
(Printexc.to_string exn) ) ;
Printexc.raise_with_backtrace exn bt
in
Command.basic ~summary ?readme (trace *> param >>| wrap)

@ -167,7 +167,6 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules =
(** command line interface *)
module Command = Core.Command
open Command.Let_syntax
let ( |*> ) a' f' = a' |> Command.Param.apply f'

@ -5,8 +5,6 @@
* LICENSE file in the root directory of this source tree.
*)
module Command = Core.Command
val main :
command:unit Command.basic_command
-> analyze:(string list -> unit -> unit) Command.Param.t

@ -10,7 +10,7 @@ module type Dom = sig
type t [@@deriving equal, sexp_of]
val pp : t pp
val report_fmt_thunk : t -> Format.formatter -> unit
val report_fmt_thunk : t -> Formatter.t -> unit
val init : Global.t iarray -> t
val join : t -> t -> t option
val is_false : t -> bool

@ -10,7 +10,7 @@
type t = Sh.t [@@deriving equal, sexp]
let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
let report_fmt_thunk = Fun.flip pp
let report_fmt_thunk = Fn.flip pp
(* set by cli *)
let simplify_states = ref true

@ -10,7 +10,7 @@
type t = Reg.Set.t [@@deriving equal, sexp]
let pp = Reg.Set.pp
let report_fmt_thunk = Fun.flip pp
let report_fmt_thunk = Fn.flip pp
let empty = Reg.Set.empty
let init globals =

@ -103,7 +103,7 @@ end = struct
let exception Found in
match
Term.Map.update s e ~f:(function
| Some _ -> raise_notrace Found
| Some _ -> Exn.raise_without_backtrace Found
| None -> e )
with
| exception Found -> None
@ -188,10 +188,10 @@ let orient e f =
let o = compare (height e) (height f) in
if o <> 0 then o else Term.compare e f
in
match Int.sign (compare e f) with
| Neg -> Some (e, f)
| Zero -> None
| Pos -> Some (f, e)
match Ordering.of_int (compare e f) with
| Less -> Some (e, f)
| Equal -> None
| Greater -> Some (f, e)
let norm (_, _, s) e = Subst.norm s e

@ -474,8 +474,9 @@ let update typ ~rcd idx ~elt =
let struct_rec key =
let memo_id = Hashtbl.create key in
let rec_app = (Term.rec_app key) Term.Record in
fun ~id typ elt_thks ->
let rec_app = (Staged.unstage (Term.rec_app key)) Term.Record in
Staged.stage
@@ fun ~id typ elt_thks ->
match Hashtbl.find memo_id id with
| None ->
(* Add placeholder to prevent computing [elts] in calls to
@ -489,12 +490,11 @@ let struct_rec key =
IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
{desc= ApN (Struct_rec, typ, elts); term} |> check invariant
| Some elts ->
(* Do not check invariant as invariant will be checked above after
the thunks are forced, before which invariant-checking may
spuriously fail. Note that it is important that the value
constructed here shares the array in the memo table, so that the
update after forcing the recursive thunks also updates this
value. *)
(* Do not check invariant as invariant will be checked above after the
thunks are forced, before which invariant-checking may spuriously
fail. Note that it is important that the value constructed here
shares the array in the memo table, so that the update after
forcing the recursive thunks also updates this value. *)
{desc= ApN (Struct_rec, typ, elts); term= rec_app ~id IArray.empty}
let size_of exp = integer Typ.siz (Z.of_int (Typ.size_of (typ exp)))

@ -188,11 +188,8 @@ val select : Typ.t -> t -> int -> t
val update : Typ.t -> rcd:t -> int -> elt:t -> t
val struct_rec :
(module Hashtbl.Key.S with type t = 'id)
-> id:'id
-> Typ.t
-> t lazy_t iarray
-> t
(module Hashtbl.Key_plain with type t = 'id)
-> (id:'id -> Typ.t -> t lazy_t iarray -> t) Staged.t
(** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
value. Cycles are detected using [Id]. The caller of [struct_rec Id]
must ensure that a single unstaging of [struct_rec Id] is used for each

@ -8,24 +8,21 @@
(** IArray - Immutable view of an array *)
open Import0
module Array = Base.Array
module Hash = Base.Hash
open Base.Continue_or_stop
(** = 'a array but covariant since imperative operations hidden *)
type +'a t
let v (a : 'a array) : 'a t = Caml.Obj.magic a
let a (v : 'a t) : 'a array = Caml.Obj.magic v
let _vl (al : 'a array list) : 'a t list = Caml.Obj.magic al
let al (vl : 'a t list) : 'a array list = Caml.Obj.magic vl
let v (a : 'a array) : 'a t = Obj.magic a
let a (v : 'a t) : 'a array = Obj.magic v
let _vl (al : 'a array list) : 'a t list = Obj.magic al
let al (vl : 'a t list) : 'a array list = Obj.magic vl
let compare cmp x y = Array.compare cmp (a x) (a y)
let equal cmp x y = Array.equal cmp (a x) (a y)
let hash_fold_t f s x = Hash.Builtin.hash_fold_array_frozen f s (a x)
let t_of_sexp a_of_sexp s = v (Array.t_of_sexp a_of_sexp s)
let sexp_of_t sexp_of_a x = Array.sexp_of_t sexp_of_a (a x)
module Infix = struct
module Import = struct
type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
end
@ -108,7 +105,9 @@ let fold_map_until xs ~init ~f ~finish =
with_return (fun {return} ->
finish
(fold_map xs ~init ~f:(fun s x ->
match f s x with Continue x -> x | Stop x -> return x )) )
match (f s x : _ Continue_or_stop.t) with
| Continue x -> x
| Stop x -> return x )) )
let concat xs = v (Array.concat (al xs))
let copy x = v (Array.copy (a x))

@ -15,7 +15,7 @@ open Import0
type +'a t [@@deriving compare, equal, hash, sexp]
module Infix : sig
module Import : sig
type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
end
@ -44,7 +44,7 @@ val fold_result :
val fold_until :
'a t
-> init:'accum
-> f:('accum -> 'a -> ('accum, 'final) Base.Continue_or_stop.t)
-> f:('accum -> 'a -> ('accum, 'final) Continue_or_stop.t)
-> finish:('accum -> 'final)
-> 'final
@ -114,7 +114,7 @@ val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
val fold_map_until :
'a t
-> init:'accum
-> f:('accum -> 'a -> ('accum * 'b, 'final) Base.Continue_or_stop.t)
-> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t)
-> finish:('accum * 'b t -> 'final)
-> 'final

@ -7,7 +7,6 @@
(** Global namespace opened in each source file by the build system *)
include Stdio
include Import0
(** Failures *)
@ -46,57 +45,78 @@ let violates f x =
assert (f x ; true) ;
assert false
type 'a or_error = ('a, exn * Caml.Printexc.raw_backtrace) result
let or_error f x () =
try Ok (f x) with exn -> Error (exn, Caml.Printexc.get_raw_backtrace ())
(** Extensions *)
module Invariant = struct
include Base.Invariant
include Core.Invariant
let invariant here t sexp_of_t f =
assert (
( try f ()
with exn ->
let bt = Caml.Printexc.get_raw_backtrace () in
let bt = Printexc.get_raw_backtrace () in
let exn =
Base.Error.to_exn
(Base.Error.create_s
(Base.Sexp.message "invariant failed"
[ ("", Sexplib.Conv.sexp_of_exn exn)
; ("", Base.Source_code_position.sexp_of_t here)
; ("", sexp_of_t t) ]))
Error.to_exn
(Error.create_s
(Sexp.List
[ Atom "invariant failed"; sexp_of_exn exn
; Source_code_position.sexp_of_t here; sexp_of_t t ]))
in
Caml.Printexc.raise_with_backtrace exn bt ) ;
Printexc.raise_with_backtrace exn bt ) ;
true )
end
module Unit = Base.Unit
(** Containers *)
type unit = Unit.t [@@deriving compare, equal, hash, sexp]
module Option = Option
include Option.Monad_infix
include Option.Monad_syntax
module List = List
module Bool = Base.Bool
module Array = struct
include Core.Array
type bool = Bool.t [@@deriving compare, equal, hash, sexp]
let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
end
module Char = Base.Char
module IArray = IArray
include IArray.Import
module Set = Set
module Map = Map
module Qset = Qset
type char = Char.t [@@deriving compare, equal, hash, sexp]
(** Data types *)
module Int = Base.Int
module String = struct
include (
Core.String :
sig
include
module type of Core.String with module Map := Core.String.Map
end )
module Map = Map.Make (Core.String)
end
type int = Int.t [@@deriving compare, equal, hash, sexp]
module Q = struct
let pp = Q.pp_print
let hash = Hashtbl.hash
let hash_fold_t s q = Int.hash_fold_t s (hash q)
let sexp_of_t q = Sexp.Atom (Q.to_string q)
let t_of_sexp = function
| Sexp.Atom s -> Q.of_string s
| _ -> assert false
module Int64 = Base.Int64
let of_z = Q.of_bigint
type int64 = Int64.t [@@deriving compare, equal, hash, sexp]
include Q
end
module Z = struct
let pp = Z.pp_print
let hash = [%hash: Z.t]
let hash_fold_t s z = Hash.fold_int s (hash z)
let hash_fold_t s z = Int.hash_fold_t s (hash z)
let sexp_of_t z = Sexp.Atom (Z.to_string z)
let t_of_sexp = function
@ -112,61 +132,3 @@ module Z = struct
include Z
end
module Q = struct
let pp = Q.pp_print
let hash = Hashtbl.hash
let hash_fold_t s q = Hash.fold_int s (hash q)
let sexp_of_t q = Sexp.Atom (Q.to_string q)
let t_of_sexp = function
| Sexp.Atom s -> Q.of_string s
| _ -> assert false
let of_z = Q.of_bigint
include Q
end
module String = struct
module T = struct
include Base.String
let hash_fold_t = Hash.fold_string
let hash = Hash.of_fold hash_fold_t
let t_of_sexp = Sexplib.Conv.string_of_sexp
let sexp_of_t = Sexplib.Conv.sexp_of_string
end
include T
module Map = Map.Make (T)
end
type string = String.t [@@deriving compare, equal, hash, sexp]
module Option = Option
type 'a option = 'a Option.t [@@deriving compare, equal, hash, sexp]
include Option.Monad_infix
include Option.Monad_syntax
module Result = Base.Result
module Array = struct
include Base.Array
let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
end
module IArray = IArray
include IArray.Infix
module List = List
type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
module Hash_queue = Core_kernel.Hash_queue
module Set = Set
module Hash_set = Base.Hash_set
module Map = Map
module Qset = Qset
module Hashtbl = Base.Hashtbl

@ -7,20 +7,8 @@
(** Global namespace opened in each source file by the build system *)
include module type of Stdio
include module type of Import0
(** Tuple operations *)
val fst3 : 'a * _ * _ -> 'a
(** First projection from a triple. *)
val snd3 : _ * 'a * _ -> 'a
(** Second projection from a triple. *)
val trd3 : _ * _ * 'a -> 'a
(** Third projection from a triple. *)
(** Function combinators *)
val ( >> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
@ -73,95 +61,63 @@ val check : ('a -> unit) -> 'a -> 'a
val violates : ('a -> unit) -> 'a -> _
(** Assert that function raises on argument. *)
type 'a or_error = ('a, exn * Caml.Printexc.raw_backtrace) result
val or_error : ('a -> 'b) -> 'a -> unit -> 'b or_error
(** [or_error f x] runs [f x] and converts unhandled exceptions to errors. *)
(** Extensions *)
module Invariant : module type of Base.Invariant
module Unit = Base.Unit
type unit = Unit.t [@@deriving compare, equal, hash, sexp]
module Invariant : module type of Core.Invariant
module Bool = Base.Bool
(** Containers *)
type bool = Bool.t [@@deriving compare, equal, hash, sexp]
module Option = Option
include module type of Option.Monad_infix
include module type of Option.Monad_syntax
module List = List
module Char = Base.Char
module Array : sig
include module type of Array
type char = Char.t [@@deriving compare, equal, hash, sexp]
val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
end
module Int = Base.Int
module IArray = IArray
include module type of IArray.Import
module Set = Set
module Map = Map
module Qset = Qset
type int = Int.t [@@deriving compare, equal, hash, sexp]
(** Data types *)
module Int64 = Base.Int64
module String : sig
include sig
include module type of Core.String with module Map := Core.String.Map
end
type int64 = Int64.t [@@deriving compare, equal, hash, sexp]
module Map : Map.S with type key = string
end
module Z : sig
include module type of struct include Z end
module Q : sig
include module type of struct include Q end
val of_z : Z.t -> t
val compare : t -> t -> int
val hash : t -> int
val hash_fold_t : t Hash.folder
val t_of_sexp : Sexp.t -> t
val sexp_of_t : t -> Sexp.t
val pp : t pp
val true_ : t
val false_ : t
val of_bool : bool -> t
val is_true : t -> bool
val is_false : t -> bool
end
module Q : sig
include module type of struct include Q end
module Z : sig
include module type of struct include Z end
val of_z : Z.t -> t
val compare : t -> t -> int
val hash : t -> int
val hash_fold_t : t Hash.folder
val t_of_sexp : Sexp.t -> t
val sexp_of_t : t -> Sexp.t
val pp : t pp
val true_ : t
val false_ : t
val of_bool : bool -> t
val is_true : t -> bool
val is_false : t -> bool
end
module String : sig
include module type of Base.String
type t = String.t [@@deriving compare, equal, hash, sexp]
module Map : Map.S with type key = string
end
type string = String.t [@@deriving compare, equal, hash, sexp]
module Option = Option
type 'a option = 'a Option.t [@@deriving compare, equal, hash, sexp]
include module type of Option.Monad_infix
include module type of Option.Monad_syntax with type 'a t = 'a option
module Result = Base.Result
module Array : sig
include module type of Base.Array
val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
end
module IArray = IArray
include module type of IArray.Infix
module List = List
type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
module Hash_queue = Core_kernel.Hash_queue
module Set = Set
module Hash_set = Base.Hash_set
module Map = Map
module Qset = Qset
module Hashtbl = Base.Hashtbl

@ -5,41 +5,22 @@
* LICENSE file in the root directory of this source tree.
*)
module Poly = struct
external ( = ) : 'a -> 'a -> bool = "%equal"
external ( <> ) : 'a -> 'a -> bool = "%notequal"
external ( < ) : 'a -> 'a -> bool = "%lessthan"
external ( > ) : 'a -> 'a -> bool = "%greaterthan"
external ( <= ) : 'a -> 'a -> bool = "%lessequal"
external ( >= ) : 'a -> 'a -> bool = "%greaterequal"
external compare : 'a -> 'a -> int = "%compare"
external equal : 'a -> 'a -> bool = "%equal"
let min x y = if x <= y then x else y
let max x y = if x >= y then x else y
end
external ( = ) : int -> int -> bool = "%equal"
external ( <> ) : int -> int -> bool = "%notequal"
external ( < ) : int -> int -> bool = "%lessthan"
external ( > ) : int -> int -> bool = "%greaterthan"
external ( <= ) : int -> int -> bool = "%lessequal"
external ( >= ) : int -> int -> bool = "%greaterequal"
let compare (a : int) b =
let int_of_bool (b : bool) = (Obj.magic b : int) in
int_of_bool (a > b) - int_of_bool (a < b)
external equal : int -> int -> bool = "%equal"
let min x y = if x <= y then x else y
let max x y = if x >= y then x else y
(** Tuple operations *)
let fst3 (x, _, _) = x
let snd3 (_, y, _) = y
let trd3 (_, _, z) = z
include (
Core :
sig
include
module type of Core
with module Printexc := Core.Printexc
and module Option := Core.Option
and module List := Core.List
and module Map := Core.Map
and module Set := Core.Set
and module String := Core.String
and type -'a return := 'a Core.return
end )
external ( == ) : 'a -> 'a -> bool = "%eq"
external ( != ) : 'a -> 'a -> bool = "%noteq"
(** Function combinators *)
@ -55,9 +36,6 @@ type 'a pp = Format.formatter -> 'a -> unit
(** Format strings. *)
type ('a, 'b) fmt = ('a, 'b) Trace.fmt
module Hash = Ppx_hash_lib.Std.Hash
module Sexp = Sexplib.Sexp
module type Applicative_syntax = sig
type 'a t
@ -71,12 +49,3 @@ module type Monad_syntax = sig
val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
end
exception Duplicate
module Return = struct type 'r t = {return: 'a. 'r -> 'a} [@@unboxed] end
let with_return (type a) f =
let module M = struct exception Return of a end in
let return a = raise_notrace (M.Return a) in
try f {Return.return} with M.Return a -> a

@ -6,7 +6,7 @@
*)
open Import0
include Base.List
include Core.List
let rec pp ?pre ?suf sep pp_elt fs = function
| [] -> ()
@ -18,7 +18,9 @@ let rec pp ?pre ?suf sep pp_elt fs = function
| xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
Option.iter suf ~f:(Format.fprintf fs)
let pop_exn = function x :: xs -> (x, xs) | [] -> raise Not_found
let pop_exn =
let not_found = Not_found_s (Atom "pop_exn") in
function x :: xs -> (x, xs) | [] -> raise not_found
let find_map_remove xs ~f =
let rec find_map_remove_ ys = function
@ -69,16 +71,18 @@ let rev_map_unzip xs ~f =
let y, z = f x in
(y :: ys, z :: zs) )
let remove_exn ?(equal = ( == )) xs x =
let remove_exn =
let not_found = Not_found_s (Atom "remove_exn") in
fun ?(equal = phys_equal) xs x ->
let rec remove_ ys = function
| [] -> raise Not_found
| [] -> raise not_found
| z :: xs ->
if equal x z then rev_append ys xs else remove_ (z :: ys) xs
in
remove_ [] xs
let remove ?equal xs x =
try Some (remove_exn ?equal xs x) with Not_found -> None
try Some (remove_exn ?equal xs x) with Not_found_s _ -> None
let rec rev_init n ~f =
if n = 0 then []
@ -88,22 +92,22 @@ let rec rev_init n ~f =
f n :: xs
let symmetric_diff ~compare xs ys =
let rec symmetric_diff_ xxs yys =
let rec symmetric_diff_ xxs yys : _ Either.t list =
match (xxs, yys) with
| x :: xs, y :: ys ->
let ord = compare x y in
if ord = 0 then symmetric_diff_ xs ys
else if ord < 0 then `Left x :: symmetric_diff_ xs yys
else `Right y :: symmetric_diff_ xxs ys
| xs, [] -> map ~f:(fun x -> `Left x) xs
| [], ys -> map ~f:(fun y -> `Right y) ys
else if ord < 0 then First x :: symmetric_diff_ xs yys
else Second y :: symmetric_diff_ xxs ys
| xs, [] -> map ~f:Either.first xs
| [], ys -> map ~f:Either.second ys
in
symmetric_diff_ (sort ~compare xs) (sort ~compare ys)
let pp_diff ~compare sep pp_elt fs (xs, ys) =
let pp_diff_elt fs elt =
match elt with
| `Left x -> Format.fprintf fs "-- %a" pp_elt x
| `Right y -> Format.fprintf fs "++ %a" pp_elt y
| First x -> Format.fprintf fs "-- %a" pp_elt x
| Second y -> Format.fprintf fs "++ %a" pp_elt y
in
pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)

@ -5,8 +5,8 @@
* LICENSE file in the root directory of this source tree.
*)
include module type of Base.List
open Import0
include module type of Core.List
val pp :
?pre:(unit, unit) fmt
@ -53,7 +53,4 @@ val remove : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list option
val rev_init : int -> f:(int -> 'a) -> 'a list
val symmetric_diff :
compare:('a -> 'a -> int)
-> 'a t
-> 'a t
-> [`Left of 'a | `Right of 'a] t
compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t

@ -5,6 +5,7 @@
* LICENSE file in the root directory of this source tree.
*)
open Import0
include Map_intf
module Make (Key : sig
@ -20,7 +21,7 @@ end) : S with type key = Key.t = struct
let compare = compare_direct
let to_map t =
Base.Map.Using_comparator.of_tree ~comparator:Key.comparator t
Core.Map.Using_comparator.of_tree ~comparator:Key.comparator t
let of_map m = Base.Map.Using_comparator.to_tree m
@ -51,7 +52,7 @@ end) : S with type key = Key.t = struct
| k, `Unequal vv ->
Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv
in
let sd = Core.Sequence.to_list (symmetric_diff ~data_equal x y) in
let sd = Sequence.to_list (symmetric_diff ~data_equal x y) in
if not (List.is_empty sd) then
Format.fprintf fs "[@[<hv>%a@]];@ " (List.pp ";@ " pp_diff_elt) sd
end

@ -13,7 +13,7 @@ module type S = sig
module Key : sig
type t = key
include Core.Comparator.S with type t := t
include Comparator.S with type t := t
end
include Core_kernel.Map_intf.Make_S_plain_tree(Key).S

@ -5,7 +5,8 @@
* LICENSE file in the root directory of this source tree.
*)
include Base.Option
open! Import0
include Core.Option
let pp fmt pp_elt fs = function
| Some x -> Format.fprintf fs fmt pp_elt x

@ -5,8 +5,8 @@
* LICENSE file in the root directory of this source tree.
*)
open Import0
include module type of Base.Option
open! Import0
include module type of Core.Option
val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp
(** Pretty-print an option. *)

@ -13,7 +13,7 @@ module type S = sig
module Elt : sig
type t = elt
include Core.Comparator.S with type t := t
include Comparator.S with type t := t
end
include Core_kernel.Set_intf.Make_S_plain_tree(Elt).S

@ -26,7 +26,7 @@ let count = ref 0
let invalid_access_count () = !count
let invalid_access fmt_thunk pp access loc =
incr count ;
Int.incr count ;
let rep fs =
Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
(loc access) pp access

@ -8,6 +8,6 @@
(** Issue reporting *)
val unknown_call : Llair.term -> unit
val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit
val invalid_access_term : (Format.formatter -> unit) -> Llair.term -> unit
val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
val invalid_access_count : unit -> int

@ -644,7 +644,7 @@ let rec norm_ s q =
[%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp_raw q]
;
let q =
map q ~f_sjn:(norm_ s) ~f_cong:Fun.id ~f_trm:(Equality.Subst.subst s)
map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s)
in
let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in
exists_fresh xs {q with cong}

@ -226,8 +226,8 @@ let assert_monomial mono =
| Mul args ->
Qset.iter args ~f:(fun factor exponent ->
assert (Q.sign exponent > 0) ;
assert_indeterminate factor |> Fun.id )
| _ -> assert_indeterminate mono |> Fun.id
assert_indeterminate factor |> Fn.id )
| _ -> assert_indeterminate mono |> Fn.id
(* a polynomial term is a monomial multiplied by a non-zero coefficient
* c × x
@ -241,8 +241,8 @@ let assert_poly_term mono coeff =
| None | Some (Integer _, _) -> assert false
| Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
) ;
assert_monomial mono |> Fun.id
| _ -> assert_monomial mono |> Fun.id
assert_monomial mono |> Fn.id
| _ -> assert_monomial mono |> Fn.id
(* a polynomial is a linear combination of monomials, e.g.
* c × x
@ -256,7 +256,7 @@ let assert_polynomial poly =
| None | Some (Integer _, _) -> assert false
| Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k))
) ;
Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fun.id)
Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
| _ -> assert false
(* aggregate args of Extract and Concat must be aggregate terms, in
@ -273,8 +273,8 @@ let invariant e =
Invariant.invariant [%here] e [%sexp_of: t]
@@ fun () ->
match e with
| Add _ -> assert_polynomial e |> Fun.id
| Mul _ -> assert_monomial e |> Fun.id
| Add _ -> assert_polynomial e |> Fn.id
| Mul _ -> assert_monomial e |> Fn.id
| Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
assert_aggregate e
| ApN (Record, elts) | RecN (Record, elts) ->
@ -783,10 +783,10 @@ let simp_uno x y = Ap2 (Uno, x, y)
let rec simp_eq x y =
match
match Int.sign (compare x y) with
| Zero -> None
| Neg -> Some (x, y)
| Pos -> Some (y, x)
match Ordering.of_int (compare x y) with
| Equal -> None
| Less -> Some (x, y)
| Greater -> Some (y, x)
with
(* e = e ==> true *)
| None -> bool true
@ -929,7 +929,8 @@ let simp_update idx rcd elt = Ap2 (Update idx, rcd, elt)
let rec_app key =
let memo_id = Hashtbl.create key in
let dummy = null in
fun ~id op elt_thks ->
Staged.stage
@@ fun ~id op elt_thks ->
match Hashtbl.find memo_id id with
| None ->
(* Add placeholder to prevent computing [elts] in calls to [rec_app]
@ -940,12 +941,11 @@ let rec_app key =
IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
RecN (op, elts) |> check invariant
| Some elts ->
(* Do not check invariant as invariant will be checked above after
the thunks are forced, before which invariant-checking may
spuriously fail. Note that it is important that the value
constructed here shares the array in the memo table, so that the
update after forcing the recursive thunks also updates this
value. *)
(* Do not check invariant as invariant will be checked above after the
thunks are forced, before which invariant-checking may spuriously
fail. Note that it is important that the value constructed here
shares the array in the memo table, so that the update after
forcing the recursive thunks also updates this value. *)
RecN (op, elts)
(* dispatching for normalization and invariant checking *)

@ -224,11 +224,8 @@ val update : rcd:t -> idx:int -> elt:t -> t
(* recursive n-ary application *)
val rec_app :
(module Hashtbl.Key.S with type t = 'id)
-> id:'id
-> recN
-> t lazy_t iarray
-> t
(module Hashtbl.Key_plain with type t = 'id)
-> (id:'id -> recN -> t lazy_t iarray -> t) Staged.t
val size_of : Typ.t -> t

Loading…
Cancel
Save