Source file Unif_subst.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
98
99

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

(** {1 Unification Substitution} *)

(** A tuple containing:

    - the substitution itself
    - delayed constraints
*)

module H = HVar

type term = Subst.term
type var = Subst.var

type t = {
  subst: Subst.t;
  cstr_l: Unif_constr.t list;
}

let subst t = t.subst
let constr_l t = t.cstr_l

let make subst cstr_l = {subst; cstr_l}

let empty : t = make Subst.empty []

let is_empty (s:t): bool =
  Subst.is_empty (subst s) &&
  CCList.is_empty (constr_l s)

let map_subst ~f t = {t with subst=f t.subst}
let of_subst s = make s []

let tags (s:t) : _ list = CCList.flat_map Unif_constr.tags (constr_l s)

let bind t v u = {t with subst=Subst.bind t.subst v u}
let update t v u = {t with subst=Subst.update t.subst v u}
let mem t v = Subst.mem t.subst v
let deref t v = Subst.deref t.subst v
let merge t1 t2 = {subst=Subst.merge t1.subst t2.subst; cstr_l = t1.cstr_l @ t2.cstr_l} 
let compose ~scope t1 t2 = {subst=Subst.FO.compose ~scope t1.subst t2.subst; cstr_l = t1.cstr_l @ t2.cstr_l}

module FO = struct
  let bind t (v:Type.t HVar.t Scoped.t) u =
    {t with subst=Subst.FO.bind t.subst (v:>InnerTerm.t HVar.t Scoped.t) u}
  let mem t (v:Type.t HVar.t Scoped.t) =
    Subst.mem t.subst (v :> InnerTerm.t HVar.t Scoped.t)
  let deref s t = Subst.FO.deref s.subst t
  let singleton v t = bind empty v t

  let rename_to_new_scope ~counter (t0, scope0) (t1, scope1) =
    let apply s t = Subst.FO.apply Subst.Renaming.none (subst s) t in
    let apply_ty s ty = Subst.Ty.apply Subst.Renaming.none (subst s) ty in
    let new_scope = if scope0 < scope1 then scope1 + 1 else scope0 + 1 in
    let add_renaming scope subst v =
      if mem subst (v,scope) 
      then subst
      else 
        let ty = apply_ty subst (HVar.ty v, scope) in
        let newvar = Term.var (H.fresh_cnt ~counter ~ty ()) in
        bind subst (v,scope) (newvar, new_scope) 
    in
    let subst = empty in
    let subst = Term.Seq.vars t0 |> Iter.fold (add_renaming scope0) subst in
    let subst = Term.Seq.vars t1 |> Iter.fold (add_renaming scope1) subst in
    let t0', t1' = apply subst (t0, scope0), apply subst (t1, scope1) in
    t0', t1', new_scope, subst
end

let has_constr t: bool = constr_l t <> []

let add_constr c t = {t with cstr_l = c :: t.cstr_l}

let pp out t: unit =
  if has_constr t
  then Format.fprintf out "(@[%a@ :constr_l (@[<hv>%a@])@])"
      Subst.pp (subst t) (Util.pp_list ~sep:"" Unif_constr.pp) (constr_l t)
  else Subst.pp out (subst t)

let equal a b =
  Subst.equal (subst a) (subst b) &&
  CCList.equal Unif_constr.equal (constr_l a) (constr_l b)

let hash a =
  Hash.combine2 (Subst.hash @@ subst a)
    (Hash.list Unif_constr.hash @@ constr_l a)

let compare a b =
  let open CCOrd.Infix in
  Subst.compare (subst a)(subst b)
  <?> (CCList.compare Unif_constr.compare, constr_l a, constr_l b)

let to_string = CCFormat.to_string pp

let constr_l_subst renaming (s:t): _ list =
  constr_l s
  |> Unif_constr.apply_subst_l renaming (subst s)