package colibrics

  1. Overview
  2. Docs

Source file cp__Type.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
type ('a, 'b) env = {
  domi: 'a Cp__Impl0.Hbi.Make.t;
  domb: 'b Cp__Impl0.Hbb.Make.t;
  mutable dirty: bool;
  mutable mi: Cp__Var0.ti list;
  mutable mb: Cp__Var0.tb list;
  }

let get_int : type xi xi1. ((xi, xi1) env) -> Cp__Var0.ti ->  xi =
  fun e b -> (Cp__Impl0.Hbi.Make.find (e.domi) b)

let get_bool : type xi2 xi3. ((xi2, xi3) env) -> Cp__Var0.tb ->  xi3 =
  fun e b -> (Cp__Impl0.Hbb.Make.find (e.domb) b)

exception Unsat

type ('a, 'b) interp = {
  i: Cp__Var0.ti -> 'a;
  b: Cp__Var0.tb -> 'b;
  }

type ('a, 'b) model = {
  modi: 'a Cp__Impl0.Hi.Make.Lock.t;
  modb: 'b Cp__Impl0.Hb.Make.Lock.t;
  }

let get_mod_int : type xi4 xi5. ((xi4, xi5) model) -> Cp__Var0.ti ->  xi4 =
  fun m v -> (Cp__Impl0.Hi.Make.Lock.find (m.modi) v)

let get_mod_bool : type xi6 xi7. ((xi6, xi7) model) -> Cp__Var0.tb ->  xi7 =
  fun m v -> (Cp__Impl0.Hb.Make.Lock.find (m.modb) v)

type 'a is_singleton =
  | Is_singleton
  | Iter of 'a