Source file Var.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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97

(* This file is free software, part of Logtk. See file "license" for more details. *)

(** {1 Variable} *)

type +'a t = {
  id: ID.t;
  ty: 'a;
}
type 'a var = 'a t

let make ~ty id = {ty; id; }

let of_string ~ty name = {ty; id=ID.make name; }

let makef ~ty msg = CCFormat.ksprintf msg ~f:(of_string ~ty)

let gensym ~ty () = {ty; id=ID.gensym(); }

let copy v = make ~ty:v.ty (ID.copy v.id)

let update_ty v ~f = {v with ty=f v.ty; }

let ty t = t.ty
let id t = t.id
let name t = t.id.ID.name

let compare a b = ID.compare a.id b.id
let equal a b = ID.equal a.id b.id
let hash a = ID.hash a.id

let pp out a = ID.pp out a.id
let to_string a = ID.to_string a.id
let pp_full out a = ID.pp_full out a.id
let pp_fullc out a = ID.pp_fullc out a.id

module Set = struct
  type 'a t = 'a var ID.Map.t
  let is_empty = ID.Map.is_empty
  let empty = ID.Map.empty
  let add t v = ID.Map.add v.id v t
  let mem t v = ID.Map.mem v.id t
  let find_exn t id = ID.Map.find id t
  let find t id = try Some (find_exn t id) with Not_found -> None
  let diff a b =
    ID.Map.merge_safe a b
      ~f:(fun _ pair -> match pair with
          | `Left x -> Some x
          | `Right _ -> None
          | `Both _ -> None)
  let cardinal t = ID.Map.cardinal t
  let intersection_empty s t =  
    try
      let _ =
        ID.Map.merge_safe s t
          ~f:(fun _ o ->
              match o with
              |  `Left _ | `Right _ -> None
              | `Both _ -> raise Exit)
      in
      true
    with Exit -> false
  let of_iter s = s |> Iter.map (fun v->v.id, v) |> ID.Map.of_iter
  let add_seq m s = s |> Iter.map (fun v->v.id, v) |> ID.Map.add_iter m
  let add_list m s = s |> List.map (fun v->v.id, v) |> ID.Map.add_list m
  let of_list l = l |> List.map (fun v->v.id,v) |> ID.Map.of_list
  let to_iter t = ID.Map.to_iter t |> Iter.map snd
  let to_list t = ID.Map.fold (fun _ v acc ->v::acc) t []
  let pp out t = Util.pp_iter ~sep:", " pp out (to_iter t)
end

module Subst = struct
  type ('a,'b) t = ('a var * 'b) ID.Map.t
  let empty = ID.Map.empty
  let is_empty = ID.Map.is_empty
  let size = ID.Map.cardinal
  let add t v x = ID.Map.add v.id (v,x) t
  let singleton v x = add empty v x
  let mem t v = ID.Map.mem v.id t
  let remove t v = ID.Map.remove v.id t
  let find_exn t v = snd (ID.Map.find v.id t)
  let find t v = try Some (find_exn t v) with Not_found -> None
  let of_list l = l |> List.map (fun (v,x)->v.id,(v,x)) |> ID.Map.of_list
  let of_iter s = s |> Iter.map (fun (v,x)->v.id, (v,x)) |> ID.Map.of_iter
  let to_iter t = ID.Map.to_iter t |> Iter.map snd
  let to_list t = ID.Map.fold (fun _ tup acc -> tup::acc) t []
  let pp pp_v out t =
    let pp_pair out (v,x) =
      Format.fprintf out "@[%a → %a@]" pp_full v pp_v x
    in
    Format.fprintf out "@[%a@]" (Util.pp_iter ~sep:", " pp_pair) (to_iter t)
  let merge a b =
    ID.Map.merge_safe a b
      ~f:(fun _ v -> match v with
          | `Both (_,x) -> Some x (* favor right one *)
          | `Left x | `Right x -> Some x)
end