Source file `coercion.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)

module E = Dolmen.Std.Expr
exception Unsupported_coercion of E.Ty.t * E.Ty.t

(* Arithmetic conversions *)
(* ************************************************************************* *)

let cst = E.Term.Const.coerce

let int_to_rat =
  let v =
    Fun.fun_1 ~cst (fun v ->
        let z = Value.extract_exn ~ops:Int.ops v in
        Rat.mk (Q.of_bigint z))
  in
  [E.Ty.int; E.Ty.rat], (fun _ -> v)

let int_to_real =
  let v =
    Fun.fun_1 ~cst (fun v ->
        let z = Value.extract_exn ~ops:Int.ops v in
        Real.mk (Q.of_bigint z))
  in
  [E.Ty.int; E.Ty.real], (fun _ -> v)

let fallback =
  let a = E.Ty.Var.mk "a" in
  let b = E.Ty.Var.mk "b" in
  [E.Ty.of_var a; E.Ty.of_var b], (fun subst ->
      let a_ty = E.Subst.Var.get a subst in
      let b_ty = E.Subst.Var.get b subst in
      raise (Unsupported_coercion (a_ty, b_ty))
    )

(* Builtins *)
(* ************************************************************************* *)

let builtins ~eval:_ _env (cst : E.Term.Const.t) =
  match cst.builtin with
  | Dolmen.Std.Builtin.Coercion ->
    Some (Fun.mk_clos @@ Fun.ad_hoc ~cst ~ty_arity:2 ~arity:1 [
        int_to_rat;
        int_to_real;
        fallback;
      ])
  | _ -> None