Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
(* Value definition *)(* ************************************************************************* *)
let ops = Value.ops ~compare:(fun b b' -> Stdlib.compare b b') ~print:(fun fmt b -> Format.fprintf fmt "%b" b) ()
(* Builtins *)(* ************************************************************************* *)
module E = Dolmen.Std.Exprmodule B = Dolmen.Std.Builtin
let true_v = Value.mk ~ops truelet false_v = Value.mk ~ops falselet mk b = if b then true_v else false_v
let fun1 f ~cst = Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> mk @@ f (Value.extract_exn ~ops x))
let fun2 f ~cst = Fun.mk_clos @@ Fun.fun_2 ~cst (fun x y -> mk @@ f (Value.extract_exn ~ops x) (Value.extract_exn ~ops y) )
let fun_n f ~cst = let func l = let l' = List.map (Value.extract_exn ~ops) l in mk (f l') in Fun.fun_n ~cst func
let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) = match cst.builtin with | B.Prop blt -> begin match blt with | T -> assert false (* Types are not evlauated *) | True -> Some true_v | False -> Some false_v | Neg -> Some (fun1 ~cst not) | And -> Some (fun_n ~cst @@ fun l -> List.fold_left (&&) true l) | Or -> Some (fun_n ~cst @@ fun l -> List.fold_left (||) false l) | Nand -> Some (fun2 ~cst (fun b1 b2 -> not (b1 && b2))) | Nor -> Some (fun2 ~cst (fun b1 b2 -> not (b1 || b2))) | Xor -> Some (fun2 ~cst (fun b1 b2 -> b1 <> b2)) | Imply -> Some (fun2 ~cst (fun b1 b2 -> not b1 || b2)) | Implied -> Some (fun2 ~cst (fun b1 b2 -> not b2 || b1)) | Equiv -> Some (fun2 ~cst (fun b1 b2 -> b1 = b2)) | Ite -> Some (Fun.mk_clos @@ Fun.fun_lazy ~cst (fun env eval args -> match args with | [cond; then_; else_] -> if Value.extract_exn ~ops (eval env cond) then eval env then_ else eval env else_ | _ -> assert false )) end | _ -> None