Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
(* Builtins *)(* ************************************************************************* *)
module E = Dolmen.Std.Exprmodule B = Dolmen.Std.Builtin
let rec all_equals = function | [] | [_] -> Bool.mk true | x :: ((y :: _) as r) -> if Value.compare x y = 0 then all_equals r else Bool.mk false
let rec distinct = function | [] | [_] -> Bool.mk true | x :: r -> if List.for_all (fun y -> Value.compare x y <> 0) r then distinct r else Bool.mk false
let builtins ~eval:_ _ (cst : E.Term.Const.t) = match cst.builtin with | B.Equal -> Some (Fun.fun_n ~cst all_equals) | B.Distinct -> Some (Fun.fun_n ~cst distinct) | _ -> None